Theorem nfeqd 2937

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

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

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 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

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

This theorem is used by:  nfeld  2938  nfeq  2940  nfned  3064  cbvexeqsetf  3472  sbcralt  3826  csbiebt  3883  csbie2df  4408  dfnfc2  4896  eusvnfb  5366  eusv2i  5367  dfid3  5561  iota2df  6527  riotaeqimp  7402  riota5f  7404  oprabid  7451  axrepndlem1  10594  axrepndlem2  10595  axunnd  10598  axpowndlem4  10602  axregndlem2  10605  axinfndlem1  10607  axinfnd  10608  axacndlem4  10612  axacndlem5  10613  axacnd  10614  bj-elgab  37634  bj-gabima  37635  wl-issetft  38296  riotasv2d  39791  nfxnegd  46215