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

Theorem nfxfrd 1580
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 1578 . 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 1553
This theorem is referenced by:  nfand  1843  nf3and  1844  nfbid  1854  nfbidOLD  1855  nfexd  1873  dvelimhw  1876  ax12olem4  2008  nfexd2  2061  dvelimf  2064  dvelimfOLD  2065  nfeud2  2292  nfmod2  2293  nfeqd  2585  nfeld  2586  nfabd2  2589  nfned  2690  nfneld  2695  nfrald  2749  nfrexd  2750  nfreud  2872  nfrmod  2873  nfsbc1d  3170  nfsbcd  3173  nfbrd  4247  nfexdwAUX7  29390  nfexdOLD7  29628  nfexd2OLD7  29655  dvelimfOLD7  29664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-nf 1554
  Copyright terms: Public domain W3C validator