Theorem nfeqd 2903

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 2723	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
2		nfv 1914	. . 3 ⊢ Ⅎ𝑦𝜑
3		nfeqd.1	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐴)
4		df-nfc 2879	. . . . . 6 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
5	3, 4	sylib 218	. . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
6	5	19.21bi 2190	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴)
7		nfeqd.2	. . . . . 6 ⊢ (𝜑 → Ⅎ𝑥𝐵)
8		df-nfc 2879	. . . . . 6 ⊢ (Ⅎ𝑥𝐵 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵)
9	7, 8	sylib 218	. . . . 5 ⊢ (𝜑 → ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐵)
10	9	19.21bi 2190	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐵)
11	6, 10	nfbid 1902	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
12	2, 11	nfald 2327	. 2 ⊢ (𝜑 → Ⅎ𝑥∀𝑦(𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵))
13	1, 12	nfxfrd 1854	1 ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-cleq 2722  df-nfc 2879

This theorem is referenced by:  nfeld  2904  nfeq  2906  nfned  3028  cbvexeqsetf  3465  sbcralt  3838  csbiebt  3894  csbie2df  4409  dfnfc2  4896  eusvnfb  5351  eusv2i  5352  dfid3  5539  iota2df  6501  riotaeqimp  7373  riota5f  7375  oprabid  7422  axrepndlem1  10552  axrepndlem2  10553  axunnd  10556  axpowndlem4  10560  axregndlem2  10563  axinfndlem1  10565  axinfnd  10566  axacndlem4  10570  axacndlem5  10571  axacnd  10572  bj-elgab  36934  bj-gabima  36935  wl-issetft  37577  riotasv2d  38957  nfxnegd  45444