Metamath Proof Explorer

Theorem ceqsalt

Description: Closed theorem version of ceqsalg . (Contributed by NM, 28-Feb-2013) (Revised by Mario Carneiro, 10-Oct-2016)

Ref Expression
Assertion ceqsalt ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∀ x x = A → φ ↔ ψ

Proof

Step Hyp Ref Expression
1 elisset ⊢ A ∈ V → ∃ x x = A
2 1 3ad2ant3 ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∃ x x = A
3 biimp ⊢ φ ↔ ψ → φ → ψ
4 3 imim3i ⊢ x = A → φ ↔ ψ → x = A → φ → x = A → ψ
5 4 al2imi ⊢ ∀ x x = A → φ ↔ ψ → ∀ x x = A → φ → ∀ x x = A → ψ
6 5 3ad2ant2 ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∀ x x = A → φ → ∀ x x = A → ψ
7 19.23t ⊢ Ⅎ x ψ → ∀ x x = A → ψ ↔ ∃ x x = A → ψ
8 7 3ad2ant1 ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∀ x x = A → ψ ↔ ∃ x x = A → ψ
9 6 8 sylibd ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∀ x x = A → φ → ∃ x x = A → ψ
10 2 9 mpid ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∀ x x = A → φ → ψ
11 biimpr ⊢ φ ↔ ψ → ψ → φ
12 11 imim2i ⊢ x = A → φ ↔ ψ → x = A → ψ → φ
13 12 com23 ⊢ x = A → φ ↔ ψ → ψ → x = A → φ
14 13 alimi ⊢ ∀ x x = A → φ ↔ ψ → ∀ x ψ → x = A → φ
15 14 3ad2ant2 ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∀ x ψ → x = A → φ
16 19.21t ⊢ Ⅎ x ψ → ∀ x ψ → x = A → φ ↔ ψ → ∀ x x = A → φ
17 16 3ad2ant1 ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∀ x ψ → x = A → φ ↔ ψ → ∀ x x = A → φ
18 15 17 mpbid ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ψ → ∀ x x = A → φ
19 10 18 impbid ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∀ x x = A → φ ↔ ψ