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

Theorem nfxfrd 1772
 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 1770 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3sylibr 223 1 (𝜒 → Ⅎ𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  Ⅎwnf 1699 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701 This theorem is referenced by:  nfand  1814  nf3and  1815  nfbid  1820  nfexd  2153  dvelimhw  2159  nfexd2  2320  dvelimf  2322  nfeud2  2470  nfmod2  2471  nfeqd  2758  nfeld  2759  nfabd2  2770  nfned  2883  nfneld  2891  nfrald  2928  nfrexd  2989  nfreud  3091  nfrmod  3092  nfsbc1d  3420  nfsbcd  3423  nfbrd  4628  bj-dvelimdv  32027  wl-nfnbi  32493  wl-sb8eut  32538
 Copyright terms: Public domain W3C validator