New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfxfrd GIF version

Theorem nfxfrd 1571
 Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
nfbii.1 (φψ)
nfxfrd.2 (χ → Ⅎxψ)
Assertion
Ref Expression
nfxfrd (χ → Ⅎxφ)

Proof of Theorem nfxfrd
StepHypRef Expression
1 nfxfrd.2 . 2 (χ → Ⅎxψ)
2 nfbii.1 . . 3 (φψ)
32nfbii 1569 . 2 (Ⅎxφ ↔ Ⅎxψ)
41, 3sylibr 203 1 (χ → Ⅎxφ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ 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:  nfand  1822  nf3and  1823  nfbid  1832  nfbidOLD  1833  nfexd  1854  nfexd2  1973  dvelimf  1997  nfeud2  2216  nfmod2  2217  nfeqd  2503  nfeld  2504  nfabd2  2507  nfned  2612  nfneld  2613  nfrald  2665  nfrexd  2666  nfreud  2783  nfrmod  2784  nfsbc1d  3063  nfsbcd  3066  nfbrd  4682
 Copyright terms: Public domain W3C validator