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

Theorem nfxfrd 1409
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 1407 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3sylibr 132 1  |-  ( ch 
->  F/ x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   F/wnf 1394
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 1381  ax-gen 1383
This theorem depends on definitions:  df-bi 115  df-nf 1395
This theorem is referenced by:  nf3and  1506  nfbid  1525  nfsbxy  1866  nfsbxyt  1867  nfeud  1964  nfmod  1965  nfeqd  2243  nfeld  2244  nfabd  2247  nfned  2349  nfneld  2358  nfraldxy  2410  nfrexdxy  2411  nfraldya  2412  nfrexdya  2413  nfsbc1d  2856  nfsbcd  2859  nfbrd  3888
  Copyright terms: Public domain W3C validator