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

Theorem nfxfrd 1854
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 1852 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3sylibr 234 1 (𝜒 → Ⅎ𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 206  df-ex 1780  df-nf 1784
This theorem is referenced by:  nfand  1898  nf3and  1899  nfbid  1903  nfexd  2321  dvelimhw  2341  nfexd2  2444  dvelimf  2446  nfmod2  2556  nfmodv  2557  nfeud2  2588  nfeudw  2589  nfeqd  2915  nfeld  2916  nfabdw  2928  nfabdwOLD  2929  nfabd  2930  nfned  3044  nfneld  3055  nfraldw  3289  nfraldwOLD  3290  nfrald  3291  nfrexd  3299  nfrexdg  3300  nfreud  3314  nfrmod  3315  nfreuwOLD  3318  nfsbc1d  3739  nfsbcdw  3742  nfsbcd  3745  nfbrd  5127  bj-dvelimdv  35076  bj-nfexd  35350  wl-sb8eut  35773
  Copyright terms: Public domain W3C validator