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

Theorem nfxfrd 1436
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
nfbii.1  |-  ( ph  <->  ps )
nfxfrd.2  |-  ( ch 
->  F/ x ps )
Assertion
Ref Expression
nfxfrd  |-  ( ch 
->  F/ x ph )

Proof of Theorem nfxfrd
StepHypRef Expression
1 nfxfrd.2 . 2  |-  ( ch 
->  F/ x ps )
2 nfbii.1 . . 3  |-  ( ph  <->  ps )
32nfbii 1434 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3sylibr 133 1  |-  ( ch 
->  F/ x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   F/wnf 1421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410
This theorem depends on definitions:  df-bi 116  df-nf 1422
This theorem is referenced by:  nf3and  1533  nfbid  1552  nfsbxy  1895  nfsbxyt  1896  nfeud  1993  nfmod  1994  nfeqd  2273  nfeld  2274  nfabd  2277  nfned  2379  nfneld  2388  nfraldxy  2444  nfrexdxy  2445  nfraldya  2446  nfrexdya  2447  nfsbc1d  2898  nfsbcd  2901  nfbrd  3943
  Copyright terms: Public domain W3C validator