Theorem nfeqd 2935

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.

Step	Hyp	Ref	Expression
1		dfcleq 2756	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
2		nfv 1944	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfeqd.1	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐴)
4		df-nfc 2912	. . . . . 6 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
5	3, 4	sylib 221	. . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
6	5	19.21bi 2225	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)
7		nfeqd.2	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐵)
8		df-nfc 2912	. . . . . 6 ⊢ (Ⅎ𝑥𝐵 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵)
9	7, 8	sylib 221	. . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵)
10	9	19.21bi 2225	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
11	6, 10	nfbid 1932	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
12	2, 11	nfald 2361	. 2 ⊢ (𝜑 → Ⅎ𝑥∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
13	1, 12	nfxfrd 1884	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  Ⅎwnf 1813   ∈ wcel 2143  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814  df-cleq 2755  df-nfc 2912

This theorem is referenced by:  nfeld  2936  nfeq  2938  nfned  3062  cbvexeqsetf  3470  sbcralt  3825  csbiebt  3882  csbie2df  4408  dfnfc2  4894  eusvnfb  5364  eusv2i  5365  dfid3  5559  iota2df  6523  riotaeqimp  7393  riota5f  7395  oprabid  7442  axrepndlem1  10572  axrepndlem2  10573  axunnd  10576  axpowndlem4  10580  axregndlem2  10583  axinfndlem1  10585  axinfnd  10586  axacndlem4  10590  axacndlem5  10591  axacnd  10592  bj-elgab  37595  bj-gabima  37596  wl-issetft  38257  riotasv2d  39751  nfxnegd  46175