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

Theorem nfxfr 1343
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfbii.1 (φψ)
nfxfr.2 xψ
Assertion
Ref Expression
nfxfr xφ

Proof of Theorem nfxfr
StepHypRef Expression
1 nfxfr.2 . 2 xψ
2 nfbii.1 . . 3 (φψ)
32nfbii 1342 . 2 (Ⅎxφ ↔ Ⅎxψ)
41, 3mpbir 134 1 xφ
Colors of variables: wff set class
Syntax hints:  wb 98  wnf 1329
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 1316  ax-gen 1318
This theorem depends on definitions:  df-bi 110  df-nf 1330
This theorem is referenced by:  nfnf1  1418  nf3an  1440  nfnf  1451  nfdc  1531  nfs1f  1645  nfeu1  1893  nfmo1  1894  sb8eu  1895  nfeu  1901  nfnfc1  2163  nfnfc  2166  nfeq  2167  nfel  2168  nfne  2275  nfnel  2282  nfra1  2333  nfre1  2343  nfreu1  2459  nfrmo1  2460  nfss  2915  rabn0m  3222  nfdisjv  3731  nfdisj1  3732  nfpo  4012  nfso  4013  nfse  4046  nfrel  4352  sb8iota  4801  nffun  4850  nffn  4921  nff  4969  nff1  5015  nffo  5030  nff1o  5049  nfiso  5371
  Copyright terms: Public domain W3C validator