ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfxfrd GIF version

Theorem nfxfrd 1451
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 1449 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3sylibr 133 1 (𝜒 → Ⅎ𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wnf 1436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425
This theorem depends on definitions:  df-bi 116  df-nf 1437
This theorem is referenced by:  nf3and  1548  nfbid  1567  nfsbxy  1913  nfsbxyt  1914  nfeud  2013  nfmod  2014  nfeqd  2294  nfeld  2295  nfabd  2298  nfned  2400  nfneld  2409  nfraldxy  2465  nfrexdxy  2466  nfraldya  2467  nfrexdya  2468  nfsbc1d  2920  nfsbcd  2923  nfbrd  3968
  Copyright terms: Public domain W3C validator