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

Theorem nfxfrd 1697
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 1695 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3sylibr 216 1  |-  ( ch 
->  F/ x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   F/wnf 1667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682
This theorem depends on definitions:  df-bi 189  df-nf 1668
This theorem is referenced by:  nfand  2008  nf3and  2009  nfbid  2016  nfexd  2035  dvelimhw  2060  nfexd2  2166  dvelimf  2168  nfeud2  2311  nfmod2  2312  nfeqd  2599  nfeld  2600  nfabd2  2611  nfned  2724  nfneld  2732  nfrald  2773  nfrexd  2849  nfreud  2963  nfrmod  2964  nfsbc1d  3285  nfsbcd  3288  nfbrd  4446  wl-nfnbi  31859  wl-sb8eut  31906
  Copyright terms: Public domain W3C validator