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

Theorem nfcxfrd 2904
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 2902 . 2 (𝑥𝐴𝑥𝐵)
41, 3sylibr 234 1 (𝜑𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wnfc 2890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-cleq 2729  df-clel 2816  df-nfc 2892
This theorem is referenced by:  nfcsb1d  3921  nfcsbd  3924  nfcsbw  3925  nfifd  4555  nfunid  4913  nfopabd  5211  nfiotadw  6517  nfiotad  6519  nfriotadw  7396  nfriotad  7399  nfovd  7460  nfttrcld  9750  nfnegd  11503  nfxnegd  45452  nfintd  49192  nfiund  49193  nfiundg  49194
  Copyright terms: Public domain W3C validator