This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfeqd

Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016)

Ref Expression
Hypotheses nfeqd.1 ⊢ φ → Ⅎ _ x A
nfeqd.2 ⊢ φ → Ⅎ _ x B
Assertion nfeqd ⊢ φ → Ⅎ x A = B

Proof

Step Hyp Ref Expression
1 nfeqd.1 ⊢ φ → Ⅎ _ x A
2 nfeqd.2 ⊢ φ → Ⅎ _ x B
3 dfcleq ⊢ A = B ↔ ∀ y y ∈ A ↔ y ∈ B
4 nfv ⊢ Ⅎ y φ
5 df-nfc ⊢ Ⅎ _ x A ↔ ∀ y Ⅎ x y ∈ A
6 1 5 sylib ⊢ φ → ∀ y Ⅎ x y ∈ A
7 6 19.21bi ⊢ φ → Ⅎ x y ∈ A
8 df-nfc ⊢ Ⅎ _ x B ↔ ∀ y Ⅎ x y ∈ B
9 2 8 sylib ⊢ φ → ∀ y Ⅎ x y ∈ B
10 9 19.21bi ⊢ φ → Ⅎ x y ∈ B
11 7 10 nfbid ⊢ φ → Ⅎ x y ∈ A ↔ y ∈ B
12 4 11 nfald ⊢ φ → Ⅎ x ∀ y y ∈ A ↔ y ∈ B
13 3 12 nfxfrd ⊢ φ → Ⅎ x A = B