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

Theorem nfxfr 1360
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 1359 . 2 (Ⅎxφ ↔ Ⅎxψ)
41, 3mpbir 134 1 xφ
Colors of variables: wff set class
Syntax hints:  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:  nfnf1  1433  nf3an  1455  nfnf  1466  nfdc  1546  nfs1f  1660  nfeu1  1908  nfmo1  1909  sb8eu  1910  nfeu  1916  nfnfc1  2178  nfnfc  2181  nfeq  2182  nfel  2183  nfne  2291  nfnel  2298  nfra1  2349  nfre1  2359  nfreu1  2475  nfrmo1  2476  nfss  2932  rabn0m  3239  nfdisjv  3748  nfdisj1  3749  nfpo  4029  nfso  4030  nfse  4063  nfrel  4368  sb8iota  4817  nffun  4867  nffn  4938  nff  4986  nff1  5033  nffo  5048  nff1o  5067  nfiso  5389
  Copyright terms: Public domain W3C validator