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

Theorem nfxfrd 1361
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 (χ → Ⅎxψ)
Assertion
Ref Expression
nfxfrd (χ → Ⅎxφ)

Proof of Theorem nfxfrd
StepHypRef Expression
1 nfxfrd.2 . 2 (χ → Ⅎxψ)
2 nfbii.1 . . 3 (φψ)
32nfbii 1359 . 2 (Ⅎxφ ↔ Ⅎxψ)
41, 3sylibr 137 1 (χ → Ⅎxφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wnf 1346
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335
This theorem depends on definitions:  df-bi 110  df-nf 1347
This theorem is referenced by:  nf3and  1458  nfbid  1477  nfsbxy  1815  nfsbxyt  1816  nfeud  1913  nfmod  1914  nfeqd  2189  nfeld  2190  nfabd  2193  nfned  2292  nfneld  2299  nfraldxy  2350  nfrexdxy  2351  nfraldya  2352  nfrexdya  2353  nfsbc1d  2774  nfsbcd  2777  nfbrd  3798
  Copyright terms: Public domain W3C validator