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

Theorem nfxfrd 1777
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 1775 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3sylibr 224 1 (𝜒 → Ⅎ𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-nf 1707
This theorem is referenced by:  nfand  1823  nf3and  1824  nfbid  1829  nfexd  2164  dvelimhw  2170  nfexd2  2331  dvelimf  2333  nfeud2  2481  nfmod2  2482  nfeqd  2768  nfeld  2769  nfabd2  2780  nfned  2891  nfneld  2901  nfrald  2939  nfrexd  3001  nfreud  3105  nfrmod  3106  nfsbc1d  3439  nfsbcd  3442  nfbrd  4663  bj-dvelimdv  32514  wl-nfnbi  32981  wl-sb8eut  33026
  Copyright terms: Public domain W3C validator