Metamath Proof Explorer

Theorem vtoclgftOLD

Description: Obsolete version of vtoclgft as of 6-Oct-2023. (Contributed by NM, 17-Feb-2013) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by JJ, 11-Aug-2021) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 elisset ⊢ A ∈ V → ∃ z z = A
2 nfnfc1 ⊢ Ⅎ x Ⅎ _ x A
3 nfcvd ⊢ Ⅎ _ x A → Ⅎ _ x z
4 id ⊢ Ⅎ _ x A → Ⅎ _ x A
5 3 4 nfeqd ⊢ Ⅎ _ x A → Ⅎ x z = A
6 eqeq1 ⊢ z = x → z = A ↔ x = A
7 6 a1i ⊢ Ⅎ _ x A → z = x → z = A ↔ x = A
8 2 5 7 cbvexd ⊢ Ⅎ _ x A → ∃ z z = A ↔ ∃ x x = A
9 1 8 syl5ib ⊢ Ⅎ _ x A → A ∈ V → ∃ x x = A
10 9 ad2antrr ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ → A ∈ V → ∃ x x = A
11 10 3impia ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ ∧ A ∈ V → ∃ x x = A
12 biimp ⊢ φ ↔ ψ → φ → ψ
13 12 imim2i ⊢ x = A → φ ↔ ψ → x = A → φ → ψ
14 13 com23 ⊢ x = A → φ ↔ ψ → φ → x = A → ψ
15 14 imp ⊢ x = A → φ ↔ ψ ∧ φ → x = A → ψ
16 15 alanimi ⊢ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ → ∀ x x = A → ψ
17 19.23t ⊢ Ⅎ x ψ → ∀ x x = A → ψ ↔ ∃ x x = A → ψ
18 17 adantl ⊢ Ⅎ _ x A ∧ Ⅎ x ψ → ∀ x x = A → ψ ↔ ∃ x x = A → ψ
19 16 18 syl5ib ⊢ Ⅎ _ x A ∧ Ⅎ x ψ → ∀ x x = A → φ ↔ ψ ∧ ∀ x φ → ∃ x x = A → ψ
20 19 imp ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ → ∃ x x = A → ψ
21 20 3adant3 ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ ∧ A ∈ V → ∃ x x = A → ψ
22 11 21 mpd ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ ∧ A ∈ V → ψ