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

Theorem nfxfrd 1861
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 1859 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3sylibr 237 1 (𝜒 → Ⅎ𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wnf 1791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817
This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792
This theorem is referenced by:  nfand  1905  nf3and  1906  nfbid  1910  nfexd  2329  dvelimhw  2347  nfexd2  2446  dvelimf  2448  nfmod2  2558  nfmodv  2559  nfeud2  2590  nfeudw  2591  nfeqd  2915  nfeld  2916  nfabdw  2928  nfabdwOLD  2929  nfabd  2930  nfned  3044  nfneld  3055  nfraldw  3145  nfraldwOLD  3146  nfrald  3147  nfrexd  3234  nfrexdg  3235  nfreud  3296  nfrmod  3297  nfreuw  3298  nfsbc1d  3726  nfsbcdw  3729  nfsbcd  3732  nfbrd  5113  bj-dvelimdv  34798  bj-nfexd  35070  wl-sb8eut  35495
  Copyright terms: Public domain W3C validator