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

Theorem nfxfrd 1820
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 1818 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3sylibr 224 1 (𝜒 → Ⅎ𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750
This theorem is referenced by:  nfand  1866  nf3and  1867  nfbid  1872  nfexd  2203  dvelimhw  2209  nfexd2  2363  dvelimf  2365  nfeud2  2510  nfmod2  2511  nfeqd  2801  nfeld  2802  nfabd2  2813  nfned  2924  nfneld  2934  nfrald  2973  nfrexd  3035  nfreud  3141  nfrmod  3142  nfsbc1d  3486  nfsbcd  3489  nfbrd  4731  bj-dvelimdv  32959  wl-nfnbi  33444  wl-sb8eut  33489
  Copyright terms: Public domain W3C validator