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

Theorem nfeqd 2801
Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
Hypotheses
Ref Expression
nfeqd.1 (𝜑𝑥𝐴)
nfeqd.2 (𝜑𝑥𝐵)
Assertion
Ref Expression
nfeqd (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)

Proof of Theorem nfeqd
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2645 . 2 (𝐴 = 𝐵 ↔ ∀𝑦(𝑦𝐴𝑦𝐵))
2 nfv 1883 . . 3 𝑦𝜑
3 nfeqd.1 . . . . 5 (𝜑𝑥𝐴)
43nfcrd 2800 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐴)
5 nfeqd.2 . . . . 5 (𝜑𝑥𝐵)
65nfcrd 2800 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
74, 6nfbid 1872 . . 3 (𝜑 → Ⅎ𝑥(𝑦𝐴𝑦𝐵))
82, 7nfald 2201 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦𝐴𝑦𝐵))
91, 8nfxfrd 1820 1 (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521   = wceq 1523  wnf 1748  wcel 2030  wnfc 2780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-cleq 2644  df-nfc 2782
This theorem is referenced by:  nfeld  2802  nfeq  2805  nfned  2924  vtoclgft  3285  vtoclgftOLD  3286  sbcralt  3543  csbiebt  3586  dfnfc2  4486  dfnfc2OLD  4487  eusvnfb  4892  eusv2i  4893  dfid3  5054  iota2df  5913  riotaeqimp  6674  riota5f  6676  oprabid  6717  axrepndlem1  9452  axrepndlem2  9453  axunnd  9456  axpowndlem4  9460  axregndlem2  9463  axinfndlem1  9465  axinfnd  9466  axacndlem4  9470  axacndlem5  9471  axacnd  9472  riotasv2d  34561  nfxnegd  39981
  Copyright terms: Public domain W3C validator