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

Theorem nfxfrd 1626
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 1624 . 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 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-nf 1600
This theorem is referenced by:  nfand  1872  nf3and  1873  nfbid  1880  nfexd  1899  dvelimhw  1902  nfexd2  2047  dvelimf  2049  nfeud2  2290  nfmod2  2291  nfeud2OLD  2302  nfeqd  2636  nfeld  2637  nfabd2  2650  nfned  2799  nfneld  2811  nfrald  2852  nfrexd  2929  nfreud  3039  nfrmod  3040  nfsbc1d  3354  nfsbcd  3357  nfbrd  4496  wl-sb8eut  29949
  Copyright terms: Public domain W3C validator