MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfxfrd Structured version   Visualization version   GIF version

Theorem nfxfrd 1847
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 (𝜒 → Ⅎ𝑥𝜓)
Assertion
Ref Expression
nfxfrd (𝜒 → Ⅎ𝑥𝜑)

Proof of Theorem nfxfrd
StepHypRef Expression
1 nfxfrd.2 . 2 (𝜒 → Ⅎ𝑥𝜓)
2 nfbii.1 . . 3 (𝜑𝜓)
32nfbii 1845 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3sylibr 235 1 (𝜒 → Ⅎ𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 208  df-ex 1774  df-nf 1778
This theorem is referenced by:  nfand  1891  nf3and  1892  nfbid  1896  nfexd  2342  dvelimhw  2360  nfexd2  2465  dvelimf  2467  nfmod2  2637  nfmodv  2638  nfeud2  2672  nfeudw  2673  nfeqd  2992  nfeld  2993  nfabdw  3004  nfabd  3005  nfabd2OLD  3007  nfned  3124  nfneld  3135  nfraldw  3227  nfrald  3228  nfrexd  3311  nfrexdg  3312  nfreud  3377  nfrmod  3378  nfreuw  3379  nfsbc1d  3793  nfsbcdw  3796  nfsbcd  3799  nfbrd  5108  bj-dvelimdv  34060  bj-nfexd  34310  wl-sb8eut  34681
  Copyright terms: Public domain W3C validator