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

Theorem nfxfr 1408
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 1407 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3mpbir 144 1 𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wb 103  wnf 1394
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383
This theorem depends on definitions:  df-bi 115  df-nf 1395
This theorem is referenced by:  nfnf1  1481  nf3an  1503  nfnf  1514  nfdc  1594  nfs1f  1710  nfeu1  1959  nfmo1  1960  sb8eu  1961  nfeu  1967  nfnfc1  2231  nfnfc  2235  nfeq  2236  nfel  2237  nfne  2348  nfnel  2357  nfra1  2409  nfre1  2419  nfreu1  2538  nfrmo1  2539  nfss  3016  rabn0m  3308  nfdisjv  3826  nfdisj1  3827  nfpo  4119  nfso  4120  nfse  4159  nffrfor  4166  nffr  4167  nfwe  4173  nfrel  4511  sb8iota  4974  nffun  5024  nffn  5096  nff  5144  nff1  5198  nffo  5216  nff1o  5235  nfiso  5567
  Copyright terms: Public domain W3C validator