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

Theorem nfxfr 1406
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 1405 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3mpbir 144 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:    <-> wb 103   F/wnf 1392
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 1379  ax-gen 1381
This theorem depends on definitions:  df-bi 115  df-nf 1393
This theorem is referenced by:  nfnf1  1479  nf3an  1501  nfnf  1512  nfdc  1592  nfs1f  1707  nfeu1  1956  nfmo1  1957  sb8eu  1958  nfeu  1964  nfnfc1  2228  nfnfc  2231  nfeq  2232  nfel  2233  nfne  2344  nfnel  2353  nfra1  2405  nfre1  2415  nfreu1  2534  nfrmo1  2535  nfss  3007  rabn0m  3299  nfdisjv  3813  nfdisj1  3814  nfpo  4102  nfso  4103  nfse  4142  nffrfor  4149  nffr  4150  nfwe  4156  nfrel  4491  sb8iota  4953  nffun  5003  nffn  5075  nff  5123  nff1  5177  nffo  5195  nff1o  5214  nfiso  5546
  Copyright terms: Public domain W3C validator