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

Theorem nfcxfrd 2903
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 2901 . 2 (𝑥𝐴𝑥𝐵)
41, 3sylibr 233 1 (𝜑𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wnfc 2884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-cleq 2725  df-clel 2811  df-nfc 2886
This theorem is referenced by:  nfcsb1d  3917  nfcsbd  3920  nfcsbw  3921  nfifd  4558  nfunid  4915  nfopabd  5217  nfiotadw  6499  nfiotad  6501  nfriotadw  7373  nfriotad  7377  nfovd  7438  nfttrcld  9705  nfnegd  11455  nfxnegd  44151  nfintd  47718  nfiund  47719  nfiundg  47720
  Copyright terms: Public domain W3C validator