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

Theorem nfcxfrd 2906
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 2904 . 2 (𝑥𝐴𝑥𝐵)
41, 3sylibr 233 1 (𝜑𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wnfc 2887
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-cleq 2728  df-clel 2814  df-nfc 2889
This theorem is referenced by:  nfcsb1d  3878  nfcsbd  3881  nfcsbw  3882  nfifd  4515  nfunid  4871  nfopabd  5173  nfiotadw  6451  nfiotad  6453  nfriotadw  7321  nfriotad  7325  nfovd  7386  nfttrcld  9646  nfnegd  11396  nfxnegd  43666  nfintd  47108  nfiund  47109  nfiundg  47110
  Copyright terms: Public domain W3C validator