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 elissetv ⊢ A ∈ V → ∃ z z = A
2 nfv ⊢ Ⅎ z Ⅎ _ x A
3 nfnfc1 ⊢ Ⅎ x Ⅎ _ x A
4 nfcvd ⊢ Ⅎ _ x A → Ⅎ _ x z
5 id ⊢ Ⅎ _ x A → Ⅎ _ x A
6 4 5 nfeqd ⊢ Ⅎ _ x A → Ⅎ x z = A
7 6 nfnd ⊢ Ⅎ _ x A → Ⅎ x ¬ z = A
8 nfvd ⊢ Ⅎ _ x A → Ⅎ z ¬ x = A
9 eqeq1 ⊢ z = x → z = A ↔ x = A
10 9 notbid ⊢ z = x → ¬ z = A ↔ ¬ x = A
11 10 a1i ⊢ Ⅎ _ x A → z = x → ¬ z = A ↔ ¬ x = A
12 2 3 7 8 11 cbv2w ⊢ Ⅎ _ x A → ∀ z ¬ z = A ↔ ∀ x ¬ x = A
13 alnex ⊢ ∀ z ¬ z = A ↔ ¬ ∃ z z = A
14 alnex ⊢ ∀ x ¬ x = A ↔ ¬ ∃ x x = A
15 12 13 14 3bitr3g ⊢ Ⅎ _ x A → ¬ ∃ z z = A ↔ ¬ ∃ x x = A
16 15 con4bid ⊢ Ⅎ _ x A → ∃ z z = A ↔ ∃ x x = A
17 1 16 imbitrid ⊢ Ⅎ _ x A → A ∈ V → ∃ x x = A
18 17 ad2antrr ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ → A ∈ V → ∃ x x = A
19 18 3impia ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ ∧ A ∈ V → ∃ x x = A
20 biimp ⊢ φ ↔ ψ → φ → ψ
21 20 imim2i ⊢ x = A → φ ↔ ψ → x = A → φ → ψ
22 21 com23 ⊢ x = A → φ ↔ ψ → φ → x = A → ψ
23 22 imp ⊢ x = A → φ ↔ ψ ∧ φ → x = A → ψ
24 23 alanimi ⊢ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ → ∀ x x = A → ψ
25 19.23t ⊢ Ⅎ x ψ → ∀ x x = A → ψ ↔ ∃ x x = A → ψ
26 25 adantl ⊢ Ⅎ _ x A ∧ Ⅎ x ψ → ∀ x x = A → ψ ↔ ∃ x x = A → ψ
27 24 26 imbitrid ⊢ Ⅎ _ x A ∧ Ⅎ x ψ → ∀ x x = A → φ ↔ ψ ∧ ∀ x φ → ∃ x x = A → ψ
28 27 imp ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ → ∃ x x = A → ψ
29 28 3adant3 ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ ∧ A ∈ V → ∃ x x = A → ψ
30 19 29 mpd ⊢ Ⅎ _ x A ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ ∧ ∀ x φ ∧ A ∈ V → ψ