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 biimp ⊢ φ ↔ ψ → φ → ψ
2 1 imim3i ⊢ x = A → φ ↔ ψ → x = A → φ → x = A → ψ
3 2 al2imi ⊢ ∀ x x = A → φ ↔ ψ → ∀ x x = A → φ → ∀ x x = A → ψ
4 elisset ⊢ A ∈ V → ∃ x x = A
5 19.23t ⊢ Ⅎ x ψ → ∀ x x = A → ψ ↔ ∃ x x = A → ψ
6 5 biimpd ⊢ Ⅎ x ψ → ∀ x x = A → ψ → ∃ x x = A → ψ
7 4 6 syl7 ⊢ Ⅎ x ψ → ∀ x x = A → ψ → A ∈ V → ψ
8 3 7 sylan9r ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → ∀ x x = A → φ → A ∈ V → ψ
9 8 com23 ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → A ∈ V → ∀ x x = A → φ → ψ
10 9 3impia ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∀ x x = A → φ → ψ
11 ceqsal1t ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → ψ → ∀ x x = A → φ
12 11 3adant3 ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ψ → ∀ x x = A → φ
13 10 12 impbid ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ A ∈ V → ∀ x x = A → φ ↔ ψ