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

Theorem nfxfrd 1577
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 1575 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3sylibr 204 1  |-  ( ch 
->  F/ x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   F/wnf 1550
This theorem is referenced by:  nfand  1833  nf3and  1834  nfbid  1844  nfbidOLD  1845  nfexd  1866  ax12olem4  1963  dvelimv  1975  nfexd2  2012  dvelimf  2031  nfeud2  2250  nfmod2  2251  nfeqd  2537  nfeld  2538  nfabd2  2541  nfned  2642  nfneld  2647  nfrald  2700  nfrexd  2701  nfreud  2823  nfrmod  2824  nfsbc1d  3121  nfsbcd  3124  nfbrd  4196  nfexdwAUX7  28791  nfexdOLD7  29007  nfexd2OLD7  29034  dvelimfOLD7  29043
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-nf 1551
  Copyright terms: Public domain W3C validator