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

Theorem nfxfrd 1950
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 1948 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3sylibr 226 1 (𝜒 → Ⅎ𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wnf 1879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905
This theorem depends on definitions:  df-bi 199  df-ex 1876  df-nf 1880
This theorem is referenced by:  nfand  1997  nf3and  1998  nfbid  2002  nfexd  2352  dvelimhw  2359  nfexd2  2453  dvelimf  2455  nfmod2  2603  nfmodv  2604  nfeud2  2630  nfeud2OLD  2641  nfmod2OLD  2642  nfeqd  2949  nfeld  2950  nfabd2  2961  nfned  3072  nfneld  3082  nfrald  3125  nfrexd  3186  nfreud  3293  nfrmod  3294  nfsbc1d  3651  nfsbcd  3654  nfbrd  4889  bj-dvelimdv  33328  wl-nfnbi  33804  wl-sb8eut  33849
  Copyright terms: Public domain W3C validator