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  2109  nfeu1  2290  nfmo1  2291  sb8eu  2298  nfnfc1  2574  nfnfc  2577  nfeq  2578  nfel  2579  nfne  2689  nfnel  2694  nfra1  2748  nfrex  2753  nfre1  2754  nfreu1  2870  nfrmo1  2871  nfrmo  2875  nfss  3333  nfdisj  4186  nfdisj1  4187  nfpo  4500  nfso  4501  nffr  4548  nfse  4549  nfwe  4550  nfrel  4954  sb8iota  5417  nffun  5468  nffn  5533  nff  5581  nff1  5629  nffo  5644  nff1o  5664  nfiso  6036  tz7.49  6694  nfixp  7073  nfdfat  27951  bnj919  29063  bnj1379  29129  bnj571  29204  bnj607  29214  bnj873  29222  bnj981  29248  bnj1039  29267  bnj1128  29286  bnj1388  29329  bnj1398  29330  bnj1417  29337  bnj1444  29339  bnj1445  29340  bnj1446  29341  bnj1449  29344  bnj1467  29350  bnj1489  29352  bnj1312  29354  bnj1518  29360  bnj1525  29365  nfexwAUX7  29378  nfs1fNEW7  29557  nfexOLD7  29615  nfnfOLD7  29616
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