MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfxfr Unicode version

Theorem nfxfr 1557
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfbii.1  |-  ( ph  <->  ps )
nfxfr.2  |-  F/ x ps
Assertion
Ref Expression
nfxfr  |-  F/ x ph

Proof of Theorem nfxfr
StepHypRef Expression
1 nfxfr.2 . 2  |-  F/ x ps
2 nfbii.1 . . 3  |-  ( ph  <->  ps )
32nfbii 1556 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3mpbir 200 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:    <-> wb 176   F/wnf 1531
This theorem is referenced by:  nfnf1  1757  nfex  1767  nfnf  1768  nfor  1770  nfan  1771  nfbi  1772  nf3or  1773  nf3an  1774  nfs1f  1970  nfeu1  2153  nfmo1  2154  sb8eu  2161  nfnfc1  2422  nfnfc  2425  nfeq  2426  nfel  2427  nfne  2539  nfnel  2540  nfra1  2593  nfrex  2598  nfre1  2599  nfreu1  2710  nfrmo1  2711  nfrmo  2715  nfss  3173  nfdisj  4005  nfdisj1  4006  nfpo  4319  nfso  4320  nffr  4367  nfse  4368  nfwe  4369  nfrel  4774  sb8iota  5226  nffun  5277  nffn  5340  nff  5387  nff1  5435  nffo  5450  nff1o  5470  nfiso  5821  tz7.49  6457  nfixp  6835  nfdfat  27993  bnj919  28797  bnj1379  28863  bnj571  28938  bnj607  28948  bnj873  28956  bnj981  28982  bnj1039  29001  bnj1128  29020  bnj1388  29063  bnj1398  29064  bnj1417  29071  bnj1444  29073  bnj1445  29074  bnj1446  29075  bnj1449  29078  bnj1467  29084  bnj1489  29086  bnj1312  29088  bnj1518  29094  bnj1525  29099
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator