Theorem nfeqd 2919

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   = wceq 1537  Ⅎwnf 1781   ∈ wcel 2108  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-cleq 2732  df-nfc 2895

This theorem is referenced by:  nfeld  2920  nfeq  2922  nfned  3050  cbvexeqsetf  3503  sbcralt  3894  csbiebt  3951  csbie2df  4466  dfnfc2  4953  eusvnfb  5411  eusv2i  5412  dfid3  5596  iota2df  6560  riotaeqimp  7431  riota5f  7433  oprabid  7480  axrepndlem1  10661  axrepndlem2  10662  axunnd  10665  axpowndlem4  10669  axregndlem2  10672  axinfndlem1  10674  axinfnd  10675  axacndlem4  10679  axacndlem5  10680  axacnd  10681  bj-elgab  36905  bj-gabima  36906  wl-issetft  37536  riotasv2d  38913  nfxnegd  45356