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

Theorem nfxfrd 1380
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 1378 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3sylibr 141 1  |-  ( ch 
->  F/ x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> 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:  nf3and  1477  nfbid  1496  nfsbxy  1834  nfsbxyt  1835  nfeud  1932  nfmod  1933  nfeqd  2208  nfeld  2209  nfabd  2212  nfned  2313  nfneld  2322  nfraldxy  2373  nfrexdxy  2374  nfraldya  2375  nfrexdya  2376  nfsbc1d  2802  nfsbcd  2805  nfbrd  3834
  Copyright terms: Public domain W3C validator