Theorem nfeqd 2758

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 2604	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
2		nfv 1830	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfeqd.1	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐴)
4	3	nfcrd 2757	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)
5		nfeqd.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝐵)
6	5	nfcrd 2757	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
7	4, 6	nfbid 1820	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
8	2, 7	nfald 2151	. 2 ⊢ (𝜑 → Ⅎ𝑥∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
9	1, 8	nfxfrd 1772	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473   = wceq 1475  Ⅎwnf 1699   ∈ wcel 1977  Ⅎwnfc 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701  df-cleq 2603  df-nfc 2740

This theorem is referenced by:  nfeld  2759  nfeq  2762  nfned  2883  vtoclgft  3227  vtoclgftOLD  3228  sbcralt  3477  csbiebt  3519  dfnfc2  4390  dfnfc2OLD  4391  eusvnfb  4788  eusv2i  4789  dfid3  4954  nfiotad  5771  iota2df  5792  riota5f  6535  oprabid  6576  axrepndlem1  9293  axrepndlem2  9294  axunnd  9297  axpowndlem4  9301  axregndlem2  9304  axinfndlem1  9306  axinfnd  9307  axacndlem4  9311  axacndlem5  9312  axacnd  9313  riotasv2d  33261  riotaeqimp  40338