NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfxfr GIF 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 (φψ)
nfxfr.2 xψ
Assertion
Ref Expression
nfxfr xφ

Proof of Theorem nfxfr
StepHypRef Expression
1 nfxfr.2 . 2 xψ
2 nfbii.1 . . 3 (φψ)
32nfbii 1569 . 2 (Ⅎxφ ↔ Ⅎxψ)
41, 3mpbir 200 1 xφ
Colors of variables: wff setvar class
Syntax hints:  wb 176  wnf 1544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557
This theorem depends on definitions:  df-bi 177  df-nf 1545
This theorem is referenced by:  nfnf1  1790  nfnan  1825  nfanOLD  1826  nf3an  1827  nfbiOLD  1835  nfor  1836  nf3or  1837  nfexOLD  1844  nfnf  1845  nfnfOLD  1846  nfs1f  2030  nfeu1  2214  nfmo1  2215  sb8eu  2222  nfnfc1  2492  nfnfc  2495  nfeq  2496  nfel  2497  nfne  2610  nfnel  2611  nfra1  2664  nfrex  2669  nfre1  2670  nfreu1  2781  nfrmo1  2782  nfrmo  2786  nfss  3266  sb8iota  4346  nffun  5130  nffn  5180  nff  5221  nff1  5256  nffo  5268  nff1o  5285  nfiso  5487
  Copyright terms: Public domain W3C validator