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

Theorem nfcxfrd 2891
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 2889 . 2 (𝑥𝐴𝑥𝐵)
41, 3sylibr 233 1 (𝜑𝑥𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1534  wnfc 2876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-nf 1779  df-cleq 2718  df-clel 2803  df-nfc 2878
This theorem is referenced by:  nfcsb1d  3915  nfcsbd  3918  nfcsbw  3919  nfifd  4562  nfunid  4919  nfopabd  5221  nfiotadw  6509  nfiotad  6511  nfriotadw  7388  nfriotad  7392  nfovd  7453  nfttrcld  9753  nfnegd  11505  nfxnegd  45056  nfintd  48419  nfiund  48420  nfiundg  48421
  Copyright terms: Public domain W3C validator