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

Theorem nfcxfrd 2981
 Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfcxfr.1 𝐴 = 𝐵
nfcxfrd.2 (𝜑𝑥𝐵)
Assertion
Ref Expression
nfcxfrd (𝜑𝑥𝐴)

Proof of Theorem nfcxfrd
StepHypRef Expression
1 nfcxfrd.2 . 2 (𝜑𝑥𝐵)
2 nfcxfr.1 . . 3 𝐴 = 𝐵
32nfceqi 2978 . 2 (𝑥𝐴𝑥𝐵)
41, 3sylibr 237 1 (𝜑𝑥𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538  Ⅎwnfc 2962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-cleq 2817  df-clel 2896  df-nfc 2964 This theorem is referenced by:  nfcsb1d  3888  nfcsbd  3891  nfcsbw  3892  nfifd  4478  nfunid  4831  nfiotadw  6306  nfiotad  6308  nfriotadw  7112  nfriotad  7115  nfovd  7175  nfnegd  10875  nfxnegd  41944  nfintd  45057  nfiund  45058  nfiundg  45059
 Copyright terms: Public domain W3C validator