Theorem nfeqd 2801

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 2645	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
2		nfv 1883	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfeqd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴)
4	3	nfcrd 2800	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)
5		nfeqd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵)
6	5	nfcrd 2800	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
7	4, 6	nfbid 1872	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
8	2, 7	nfald 2201	. 2 ⊢ (𝜑 → Ⅎ𝑥∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
9	1, 8	nfxfrd 1820	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1521   = wceq 1523  Ⅎwnf 1748   ∈ wcel 2030  Ⅎwnfc 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-cleq 2644  df-nfc 2782

This theorem is referenced by:  nfeld  2802  nfeq  2805  nfned  2924  vtoclgft  3285  vtoclgftOLD  3286  sbcralt  3543  csbiebt  3586  dfnfc2  4486  dfnfc2OLD  4487  eusvnfb  4892  eusv2i  4893  dfid3  5054  iota2df  5913  riotaeqimp  6674  riota5f  6676  oprabid  6717  axrepndlem1  9452  axrepndlem2  9453  axunnd  9456  axpowndlem4  9460  axregndlem2  9463  axinfndlem1  9465  axinfnd  9466  axacndlem4  9470  axacndlem5  9471  axacnd  9472  riotasv2d  34561  nfxnegd  39981