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

Theorem nfxfr 1579
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 1578 . 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 1553
This theorem is referenced by:  nfnf1  1808  nfnan  1847  nfanOLD  1848  nf3an  1849  nfbiOLD  1857  nfor  1858  nf3or  1859  nfexOLD  1866  nfnf  1867  nfnfOLD  1868  nfs1f  2120  nfeu1  2291  nfmo1  2292  sb8eu  2299  nfnfc1  2575  nfnfc  2578  nfeq  2579  nfel  2580  nfne  2695  nfnel  2702  nfra1  2756  nfrex  2761  nfre1  2762  nfreu1  2878  nfrmo1  2879  nfrmo  2883  nfss  3341  nfdisj  4194  nfdisj1  4195  nfpo  4508  nfso  4509  nffr  4556  nfse  4557  nfwe  4558  nfrel  4962  sb8iota  5425  nffun  5476  nffn  5541  nff  5589  nff1  5637  nffo  5652  nff1o  5672  nfiso  6044  tz7.49  6702  nfixp  7081  nfdfat  27970  bnj919  29136  bnj1379  29202  bnj571  29277  bnj607  29287  bnj873  29295  bnj981  29321  bnj1039  29340  bnj1128  29359  bnj1388  29402  bnj1398  29403  bnj1417  29410  bnj1444  29412  bnj1445  29413  bnj1446  29414  bnj1449  29417  bnj1467  29423  bnj1489  29425  bnj1312  29427  bnj1518  29433  bnj1525  29438  nfexwAUX7  29451  nfs1fNEW7  29630  nfexOLD7  29688  nfnfOLD7  29689
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-nf 1554
  Copyright terms: Public domain W3C validator