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

Theorem nfxfrd 1651
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 1649 . 2  |-  ( F/ x ph  <->  F/ x ps )
41, 3sylibr 212 1  |-  ( ch 
->  F/ x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636
This theorem depends on definitions:  df-bi 185  df-nf 1622
This theorem is referenced by:  nfand  1930  nf3and  1931  nfbid  1938  nfexd  1957  dvelimhw  1960  nfexd2  2078  dvelimf  2080  nfeud2  2298  nfmod2  2299  nfeqd  2623  nfeld  2624  nfabd2  2637  nfned  2786  nfneld  2798  nfrald  2839  nfrexd  2916  nfreud  3027  nfrmod  3028  nfsbc1d  3342  nfsbcd  3345  nfbrd  4482  wl-nfnbi  30219  wl-sb8eut  30262
  Copyright terms: Public domain W3C validator