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

Theorem nfxfr 1474
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 1473 . 2 (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
41, 3mpbir 146 1 𝑥𝜑
Colors of variables: wff set class
Syntax hints:  wb 105  wnf 1460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449
This theorem depends on definitions:  df-bi 117  df-nf 1461
This theorem is referenced by:  nfnf1  1544  nf3an  1566  nfnf  1577  nfdc  1659  nfs1f  1780  nfsbv  1947  nfeu1  2037  nfmo1  2038  sb8eu  2039  nfeu  2045  nfnfc1  2322  nfnfc  2326  nfeq  2327  nfel  2328  nfabdw  2338  nfne  2440  nfnel  2449  nfra1  2508  nfre1  2520  nfreu1  2649  nfrmo1  2650  nfss  3150  rabn0m  3452  nfdisjv  3994  nfdisj1  3995  nfpo  4303  nfso  4304  nfse  4343  nffrfor  4350  nffr  4351  nfwe  4357  nfrel  4713  sb8iota  5187  nffun  5241  nffn  5314  nff  5364  nff1  5421  nffo  5439  nff1o  5461  nfiso  5809  nfixpxy  6719
  Copyright terms: Public domain W3C validator