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

Theorem nfxfrd 1694
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 1692 . 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 1664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679
This theorem depends on definitions:  df-bi 189  df-nf 1665
This theorem is referenced by:  nfand  1982  nf3and  1983  nfbid  1990  nfexd  2009  dvelimhw  2012  nfexd2  2130  dvelimf  2132  nfeud2  2279  nfmod2  2280  nfeqd  2592  nfeld  2593  nfabd2  2606  nfned  2758  nfneld  2770  nfrald  2811  nfrexd  2888  nfreud  3002  nfrmod  3003  nfsbc1d  3318  nfsbcd  3321  nfbrd  4465  wl-nfnbi  31779  wl-sb8eut  31826
  Copyright terms: Public domain W3C validator