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

Theorem nfeqd 2913
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 2727 . 2 (𝐴 = 𝐵 ↔ ∀𝑦(𝑦𝐴𝑦𝐵))
2 nfv 1911 . . 3 𝑦𝜑
3 nfeqd.1 . . . . . 6 (𝜑𝑥𝐴)
4 df-nfc 2889 . . . . . 6 (𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
53, 4sylib 218 . . . . 5 (𝜑 → ∀𝑦𝑥 𝑦𝐴)
6519.21bi 2186 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐴)
7 nfeqd.2 . . . . . 6 (𝜑𝑥𝐵)
8 df-nfc 2889 . . . . . 6 (𝑥𝐵 ↔ ∀𝑦𝑥 𝑦𝐵)
97, 8sylib 218 . . . . 5 (𝜑 → ∀𝑦𝑥 𝑦𝐵)
10919.21bi 2186 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
116, 10nfbid 1899 . . 3 (𝜑 → Ⅎ𝑥(𝑦𝐴𝑦𝐵))
122, 11nfald 2326 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦𝐴𝑦𝐵))
131, 12nfxfrd 1850 1 (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1534   = wceq 1536  wnf 1779  wcel 2105  wnfc 2887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-nf 1780  df-cleq 2726  df-nfc 2889
This theorem is referenced by:  nfeld  2914  nfeq  2916  nfned  3041  cbvexeqsetf  3492  sbcralt  3880  csbiebt  3937  csbie2df  4448  dfnfc2  4933  eusvnfb  5398  eusv2i  5399  dfid3  5585  iota2df  6549  riotaeqimp  7413  riota5f  7415  oprabid  7462  axrepndlem1  10629  axrepndlem2  10630  axunnd  10633  axpowndlem4  10637  axregndlem2  10640  axinfndlem1  10642  axinfnd  10643  axacndlem4  10647  axacndlem5  10648  axacnd  10649  bj-elgab  36921  bj-gabima  36922  wl-issetft  37562  riotasv2d  38938  nfxnegd  45390
  Copyright terms: Public domain W3C validator