Theorem nfeqd 2933

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 2754	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
2		nfv 1947	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfeqd.1	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐴)
4		df-nfc 2910	. . . . . 6 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
5	3, 4	sylib 221	. . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
6	5	19.21bi 2226	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)
7		nfeqd.2	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐵)
8		df-nfc 2910	. . . . . 6 ⊢ (Ⅎ𝑥𝐵 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵)
9	7, 8	sylib 221	. . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵)
10	9	19.21bi 2226	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
11	6, 10	nfbid 1935	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
12	2, 11	nfald 2359	. 2 ⊢ (𝜑 → Ⅎ𝑥∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
13	1, 12	nfxfrd 1887	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2145  Ⅎwnfc 2908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-cleq 2753  df-nfc 2910

This theorem is used by:  nfeld  2934  nfeq  2936  nfned  3060  cbvexeqsetf  3466  sbcralt  3819  csbiebt  3876  csbie2df  4401  dfnfc2  4889  eusvnfb  5355  eusv2i  5356  dfid3  5549  iota2df  6525  riotaeqimp  7403  riota5f  7405  oprabid  7452  axrepndlem1  10677  axrepndlem2  10678  axunnd  10681  axpowndlem4  10685  axregndlem2  10688  axinfndlem1  10690  axinfnd  10691  axacndlem4  10695  axacndlem5  10696  axacnd  10697  bj-elgab  37852  bj-gabima  37853  wl-issetft  38514  riotasv2d  40014  nfxnegd  46450