Theorem vtoclgft 3492

Description: Closed theorem form of vtoclgf 3503. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by JJ, 11-Aug-2021.) Avoid ax-13 2372. (Revised by Gino Giotto, 6-Oct-2023.)

Assertion

Ref	Expression
vtoclgft	⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓)

Proof of Theorem vtoclgft

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elisset 2820	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → ∃𝑧 𝑧 = 𝐴)
2		nfv 1917	. . . . . . . . 9 ⊢ Ⅎ𝑧Ⅎ𝑥𝐴
3		nfnfc1 2910	. . . . . . . . 9 ⊢ Ⅎ𝑥Ⅎ𝑥𝐴
4		nfcvd 2908	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥𝑧)
5		id 22	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥𝐴)
6	4, 5	nfeqd 2917	. . . . . . . . . 10 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑧 = 𝐴)
7	6	nfnd 1861	. . . . . . . . 9 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 ¬ 𝑧 = 𝐴)
8		nfvd 1918	. . . . . . . . 9 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑧 ¬ 𝑥 = 𝐴)
9		eqeq1 2742	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴))
10	9	a1i 11	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥𝐴 → (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴)))
11		notbi 319	. . . . . . . . . . 11 ⊢ ((𝑧 = 𝐴 ↔ 𝑥 = 𝐴) ↔ (¬ 𝑧 = 𝐴 ↔ ¬ 𝑥 = 𝐴))
12	10, 11	syl6ib 250	. . . . . . . . . 10 ⊢ (Ⅎ𝑥𝐴 → (𝑧 = 𝑥 → (¬ 𝑧 = 𝐴 ↔ ¬ 𝑥 = 𝐴)))
13		biimp 214	. . . . . . . . . 10 ⊢ ((¬ 𝑧 = 𝐴 ↔ ¬ 𝑥 = 𝐴) → (¬ 𝑧 = 𝐴 → ¬ 𝑥 = 𝐴))
14	12, 13	syl6 35	. . . . . . . . 9 ⊢ (Ⅎ𝑥𝐴 → (𝑧 = 𝑥 → (¬ 𝑧 = 𝐴 → ¬ 𝑥 = 𝐴)))
15	2, 3, 7, 8, 14	cbv1v 2333	. . . . . . . 8 ⊢ (Ⅎ𝑥𝐴 → (∀𝑧 ¬ 𝑧 = 𝐴 → ∀𝑥 ¬ 𝑥 = 𝐴))
16		equcomi 2020	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → 𝑧 = 𝑥)
17		biimpr 219	. . . . . . . . . 10 ⊢ ((¬ 𝑧 = 𝐴 ↔ ¬ 𝑥 = 𝐴) → (¬ 𝑥 = 𝐴 → ¬ 𝑧 = 𝐴))
18	16, 12, 17	syl56 36	. . . . . . . . 9 ⊢ (Ⅎ𝑥𝐴 → (𝑥 = 𝑧 → (¬ 𝑥 = 𝐴 → ¬ 𝑧 = 𝐴)))
19	3, 2, 8, 7, 18	cbv1v 2333	. . . . . . . 8 ⊢ (Ⅎ𝑥𝐴 → (∀𝑥 ¬ 𝑥 = 𝐴 → ∀𝑧 ¬ 𝑧 = 𝐴))
20	15, 19	impbid 211	. . . . . . 7 ⊢ (Ⅎ𝑥𝐴 → (∀𝑧 ¬ 𝑧 = 𝐴 ↔ ∀𝑥 ¬ 𝑥 = 𝐴))
21		alnex 1784	. . . . . . 7 ⊢ (∀𝑧 ¬ 𝑧 = 𝐴 ↔ ¬ ∃𝑧 𝑧 = 𝐴)
22		alnex 1784	. . . . . . 7 ⊢ (∀𝑥 ¬ 𝑥 = 𝐴 ↔ ¬ ∃𝑥 𝑥 = 𝐴)
23	20, 21, 22	3bitr3g 313	. . . . . 6 ⊢ (Ⅎ𝑥𝐴 → (¬ ∃𝑧 𝑧 = 𝐴 ↔ ¬ ∃𝑥 𝑥 = 𝐴))
24	23	con4bid 317	. . . . 5 ⊢ (Ⅎ𝑥𝐴 → (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴))
25	1, 24	syl5ib 243	. . . 4 ⊢ (Ⅎ𝑥𝐴 → (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴))
26	25	ad2antrr 723	. . 3 ⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑)) → (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴))
27	26	3impia 1116	. 2 ⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → ∃𝑥 𝑥 = 𝐴)
28		biimp 214	. . . . . . . . 9 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
29	28	imim2i 16	. . . . . . . 8 ⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝑥 = 𝐴 → (𝜑 → 𝜓)))
30	29	com23 86	. . . . . . 7 ⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝜑 → (𝑥 = 𝐴 → 𝜓)))
31	30	imp 407	. . . . . 6 ⊢ (((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝜑) → (𝑥 = 𝐴 → 𝜓))
32	31	alanimi 1819	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) → ∀𝑥(𝑥 = 𝐴 → 𝜓))
33		19.23t 2203	. . . . . 6 ⊢ (Ⅎ𝑥𝜓 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)))
34	33	adantl 482	. . . . 5 ⊢ ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)))
35	32, 34	syl5ib 243	. . . 4 ⊢ ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) → ((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) → (∃𝑥 𝑥 = 𝐴 → 𝜓)))
36	35	imp 407	. . 3 ⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑)) → (∃𝑥 𝑥 = 𝐴 → 𝜓))
37	36	3adant3 1131	. 2 ⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → (∃𝑥 𝑥 = 𝐴 → 𝜓))
38	27, 37	mpd 15	1 ⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086  ∀wal 1537   = wceq 1539  ∃wex 1782  Ⅎwnf 1786   ∈ wcel 2106  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889

This theorem is referenced by:  vtocldf  3493  bj-vtoclgfALT  35230