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

Theorem nfxfr 1570
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 1569 . 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 1544
This theorem is referenced by:  nfnf1  1791  nfnan  1830  nfanOLD  1831  nf3an  1832  nfbiOLD  1840  nfor  1841  nf3or  1842  nfexOLD  1849  nfnf  1850  nfnfOLD  1851  nfs1f  2035  nfeu1  2219  nfmo1  2220  sb8eu  2227  nfnfc1  2497  nfnfc  2500  nfeq  2501  nfel  2502  nfne  2615  nfnel  2616  nfra1  2669  nfrex  2674  nfre1  2675  nfreu1  2786  nfrmo1  2787  nfrmo  2791  nfss  3249  nfdisj  4086  nfdisj1  4087  nfpo  4401  nfso  4402  nffr  4449  nfse  4450  nfwe  4451  nfrel  4856  sb8iota  5308  nffun  5359  nffn  5422  nff  5470  nff1  5518  nffo  5533  nff1o  5553  nfiso  5908  tz7.49  6544  nfixp  6923  nfdfat  27318  bnj919  28559  bnj1379  28625  bnj571  28700  bnj607  28710  bnj873  28718  bnj981  28744  bnj1039  28763  bnj1128  28782  bnj1388  28825  bnj1398  28826  bnj1417  28833  bnj1444  28835  bnj1445  28836  bnj1446  28837  bnj1449  28840  bnj1467  28846  bnj1489  28848  bnj1312  28850  bnj1518  28856  bnj1525  28861  nfexwAUX7  28874  nfs1fNEW7  29048  nfexOLD7  29089  nfnfOLD7  29090
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557
This theorem depends on definitions:  df-bi 177  df-nf 1545
  Copyright terms: Public domain W3C validator