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

Theorem nfeqd 2916
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 2730 . 2 (𝐴 = 𝐵 ↔ ∀𝑦(𝑦𝐴𝑦𝐵))
2 nfv 1914 . . 3 𝑦𝜑
3 nfeqd.1 . . . . . 6 (𝜑𝑥𝐴)
4 df-nfc 2892 . . . . . 6 (𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
53, 4sylib 218 . . . . 5 (𝜑 → ∀𝑦𝑥 𝑦𝐴)
6519.21bi 2189 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐴)
7 nfeqd.2 . . . . . 6 (𝜑𝑥𝐵)
8 df-nfc 2892 . . . . . 6 (𝑥𝐵 ↔ ∀𝑦𝑥 𝑦𝐵)
97, 8sylib 218 . . . . 5 (𝜑 → ∀𝑦𝑥 𝑦𝐵)
10919.21bi 2189 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
116, 10nfbid 1902 . . 3 (𝜑 → Ⅎ𝑥(𝑦𝐴𝑦𝐵))
122, 11nfald 2328 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦𝐴𝑦𝐵))
131, 12nfxfrd 1854 1 (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538   = wceq 1540  wnf 1783  wcel 2108  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-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-cleq 2729  df-nfc 2892
This theorem is referenced by:  nfeld  2917  nfeq  2919  nfned  3044  cbvexeqsetf  3495  sbcralt  3872  csbiebt  3928  csbie2df  4443  dfnfc2  4929  eusvnfb  5393  eusv2i  5394  dfid3  5581  iota2df  6548  riotaeqimp  7414  riota5f  7416  oprabid  7463  axrepndlem1  10632  axrepndlem2  10633  axunnd  10636  axpowndlem4  10640  axregndlem2  10643  axinfndlem1  10645  axinfnd  10646  axacndlem4  10650  axacndlem5  10651  axacnd  10652  bj-elgab  36940  bj-gabima  36941  wl-issetft  37583  riotasv2d  38958  nfxnegd  45452
  Copyright terms: Public domain W3C validator