ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfxfr Unicode 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  |-  ( ph  <->  ps )
nfxfr.2  |-  F/ x ps
Assertion
Ref Expression
nfxfr  |-  F/ x ph

Proof of Theorem nfxfr
StepHypRef Expression
1 nfxfr.2 . 2  |-  F/ x ps
2 nfbii.1 . . 3  |-  ( ph  <->  ps )
32nfbii 1473 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3mpbir 146 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:    <-> wb 105   F/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  3149  rabn0m  3451  nfdisjv  3993  nfdisj1  3994  nfpo  4302  nfso  4303  nfse  4342  nffrfor  4349  nffr  4350  nfwe  4356  nfrel  4712  sb8iota  5186  nffun  5240  nffn  5313  nff  5363  nff1  5420  nffo  5438  nff1o  5460  nfiso  5807  nfixpxy  6717
  Copyright terms: Public domain W3C validator