ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfxfr Unicode 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  |-  ( 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 1378 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3mpbir 138 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:    <-> wb 102   F/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  2965  rabn0m  3272  nfdisjv  3784  nfdisj1  3785  nfpo  4065  nfso  4066  nfse  4105  nffrfor  4112  nffr  4113  nfwe  4119  nfrel  4452  sb8iota  4901  nffun  4951  nffn  5022  nff  5070  nff1  5117  nffo  5132  nff1o  5151  nfiso  5473
  Copyright terms: Public domain W3C validator