Metamath Proof Explorer

Theorem vtoclgft

Description: Closed theorem form of vtoclgf . The reverse implication is proven in ceqsal1t . See ceqsalt for a version with x and A disjoint. (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by JJ, 11-Aug-2021) Avoid ax-13 . (Revised by Gino Giotto, 6-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ V → A ∈ V
2 issetft ⊢ Ⅎ _ x A → A ∈ V ↔ ∃ x x = A
3 1 2 imbitrid ⊢ Ⅎ _ x A → A ∈ V → ∃ x x = A
4 3 ad2antrr ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ → A ∈ V → ∃ x x = A
5 4 3impia ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ ∧ A ∈ V → ∃ x x = A
6 biimp ⊢ φ ↔ ψ → φ → ψ
7 6 imim2i ⊢ x = A → φ ↔ ψ → x = A → φ → ψ
8 7 com23 ⊢ x = A → φ ↔ ψ → φ → x = A → ψ
9 8 imp ⊢ x = A → φ ↔ ψ ∧ φ → x = A → ψ
10 9 alanimi ⊢ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ → ∀ x x = A → ψ
11 19.23t ⊢ Ⅎ x ψ → ∀ x x = A → ψ ↔ ∃ x x = A → ψ
12 11 adantl ⊢ Ⅎ _ x A ∧ Ⅎ x ψ → ∀ x x = A → ψ ↔ ∃ x x = A → ψ
13 10 12 imbitrid ⊢ Ⅎ _ x A ∧ Ⅎ x ψ → ∀ x x = A → φ ↔ ψ ∧ ∀ x φ → ∃ x x = A → ψ
14 13 imp ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ → ∃ x x = A → ψ
15 14 3adant3 ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ ∧ A ∈ V → ∃ x x = A → ψ
16 5 15 mpd ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ ∧ A ∈ V → ψ