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

Theorem nfxfr 1451
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 1450 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3mpbir 145 1 𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wb 104  wnf 1437
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 1424  ax-gen 1426
This theorem depends on definitions:  df-bi 116  df-nf 1438
This theorem is referenced by:  nfnf1  1524  nf3an  1546  nfnf  1557  nfdc  1638  nfs1f  1754  nfeu1  2011  nfmo1  2012  sb8eu  2013  nfeu  2019  nfnfc1  2285  nfnfc  2289  nfeq  2290  nfel  2291  nfne  2402  nfnel  2411  nfra1  2469  nfre1  2479  nfreu1  2605  nfrmo1  2606  nfss  3093  rabn0m  3393  nfdisjv  3924  nfdisj1  3925  nfpo  4229  nfso  4230  nfse  4269  nffrfor  4276  nffr  4277  nfwe  4283  nfrel  4630  sb8iota  5101  nffun  5152  nffn  5225  nff  5275  nff1  5332  nffo  5350  nff1o  5371  nfiso  5713  nfixpxy  6617
  Copyright terms: Public domain W3C validator