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

Theorem nfxfr 1576
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 1575 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3mpbir 201 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:    <-> wb 177   F/wnf 1550
This theorem is referenced by:  nfnf1  1804  nfnan  1843  nfanOLD  1844  nf3an  1845  nfbiOLD  1853  nfor  1854  nf3or  1855  nfexOLD  1862  nfnf  1863  nfnfOLD  1864  nfs1f  2083  nfeu1  2268  nfmo1  2269  sb8eu  2276  nfnfc1  2547  nfnfc  2550  nfeq  2551  nfel  2552  nfne  2662  nfnel  2667  nfra1  2720  nfrex  2725  nfre1  2726  nfreu1  2842  nfrmo1  2843  nfrmo  2847  nfss  3305  nfdisj  4158  nfdisj1  4159  nfpo  4472  nfso  4473  nffr  4520  nfse  4521  nfwe  4522  nfrel  4925  sb8iota  5388  nffun  5439  nffn  5504  nff  5552  nff1  5600  nffo  5615  nff1o  5635  nfiso  6007  tz7.49  6665  nfixp  7044  nfdfat  27865  bnj919  28846  bnj1379  28912  bnj571  28987  bnj607  28997  bnj873  29005  bnj981  29031  bnj1039  29050  bnj1128  29069  bnj1388  29112  bnj1398  29113  bnj1417  29120  bnj1444  29122  bnj1445  29123  bnj1446  29124  bnj1449  29127  bnj1467  29133  bnj1489  29135  bnj1312  29137  bnj1518  29143  bnj1525  29148  nfexwAUX7  29161  nfs1fNEW7  29335  nfexOLD7  29376  nfnfOLD7  29377
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-nf 1551
  Copyright terms: Public domain W3C validator