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

Theorem nfxfrd 1930
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 1928 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3sylibr 224 1 (𝜒 → Ⅎ𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-ex 1853  df-nf 1858
This theorem is referenced by:  nfand  1978  nf3and  1979  nfbid  1984  nfexd  2329  dvelimhw  2338  nfexd2  2482  dvelimf  2484  nfeud2  2630  nfmod2  2631  nfeqd  2921  nfeld  2922  nfabd2  2933  nfned  3044  nfneld  3054  nfrald  3093  nfrexd  3154  nfreud  3260  nfrmod  3261  nfsbc1d  3606  nfsbcd  3609  nfbrd  4833  bj-dvelimdv  33169  wl-nfnbi  33650  wl-sb8eut  33694
  Copyright terms: Public domain W3C validator