Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfxfr GIF 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  2966  rabn0m  3273  nfdisjv  3785  nfdisj1  3786  nfpo  4066  nfso  4067  nfse  4106  nffrfor  4113  nffr  4114  nfwe  4120  nfrel  4453  sb8iota  4902  nffun  4952  nffn  5023  nff  5071  nff1  5118  nffo  5133  nff1o  5152  nfiso  5474
 Copyright terms: Public domain W3C validator