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 206  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 207  df-ex 1780  df-nf 1784
This theorem is referenced by:  nfand  1897  nf3and  1898  nfbid  1902  nfexd  2329  dvelimhw  2347  nfexd2  2451  dvelimf  2453  nfmod2  2558  nfmodv  2559  nfeud2  2590  nfeudw  2591  nfeqd  2916  nfeld  2917  nfabdw  2927  nfabd  2928  nfned  3044  nfneld  3055  nfraldw  3309  nfrexdw  3310  nfrald  3372  nfrexd  3373  nfreuwOLD  3426  nfrmod  3432  nfreud  3433  nfsbc1d  3806  nfsbcdw  3809  nfsbcd  3812  nfbrd  5189  bj-dvelimdv  36852  bj-nfexd  37139  wl-sb8eut  37579  wl-sb8eutv  37580
  Copyright terms: Public domain W3C validator