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

Theorem nfxfrd 1561
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 1559 . 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 1534
This theorem is referenced by:  nfbid  1774  nfand  1775  nf3and  1776  nfexd  1788  nfexd2  1926  dvelimf  1950  nfeud2  2168  nfmod2  2169  nfeqd  2446  nfeld  2447  nfabd2  2450  nfned  2554  nfneld  2555  nfrald  2607  nfrexd  2608  nfreud  2725  nfrmod  2726  nfsbc1d  3021  nfsbcd  3024  nfbrd  4082  nfexdwAUX7  29430  nfexdOLD7  29645  nfexd2OLD7  29672  dvelimfOLD7  29681
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-nf 1535
  Copyright terms: Public domain W3C validator