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

Theorem nfxfr 1379
 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
Assertion
Ref Expression
nfxfr

Proof of Theorem nfxfr
StepHypRef Expression
1 nfxfr.2 . 2
2 nfbii.1 . . 3
32nfbii 1378 . 2
41, 3mpbir 138 1
 Colors of variables: wff set class Syntax hints:   wb 102  wnf 1365 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354 This theorem depends on definitions:  df-bi 114  df-nf 1366 This theorem is referenced by:  nfnf1  1452  nf3an  1474  nfnf  1485  nfdc  1565  nfs1f  1679  nfeu1  1927  nfmo1  1928  sb8eu  1929  nfeu  1935  nfnfc1  2197  nfnfc  2200  nfeq  2201  nfel  2202  nfne  2312  nfnel  2321  nfra1  2372  nfre1  2382  nfreu1  2498  nfrmo1  2499  nfss  2965  rabn0m  3272  nfdisjv  3784  nfdisj1  3785  nfpo  4065  nfso  4066  nfse  4105  nffrfor  4112  nffr  4113  nfwe  4119  nfrel  4452  sb8iota  4901  nffun  4951  nffn  5022  nff  5070  nff1  5117  nffo  5132  nff1o  5151  nfiso  5473
 Copyright terms: Public domain W3C validator