MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfxfrd Unicode version

Theorem nfxfrd 1558
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 1556 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3sylibr 203 1  |-  ( ch 
->  F/ x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   F/wnf 1531
This theorem is referenced by:  nfbid  1762  nfand  1763  nf3and  1764  nfexd  1776  nfexd2  1913  dvelimf  1937  nfeud2  2155  nfmod2  2156  nfeqd  2433  nfeld  2434  nfabd2  2437  nfned  2541  nfneld  2542  nfrald  2594  nfrexd  2595  nfreud  2712  nfrmod  2713  nfsbc1d  3008  nfsbcd  3011  nfbrd  4066
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-nf 1532
  Copyright terms: Public domain W3C validator