Theorem vtoclgft 3482

Description: Closed theorem form of vtoclgf 3493. (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 1918	. . . . . . . . 9 ⊢ Ⅎ𝑧Ⅎ𝑥𝐴
3		nfnfc1 2909	. . . . . . . . 9 ⊢ Ⅎ𝑥Ⅎ𝑥𝐴
4		nfcvd 2907	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥𝑧)
5		id 22	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥𝐴)
6	4, 5	nfeqd 2916	. . . . . . . . . 10 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑧 = 𝐴)
7	6	nfnd 1862	. . . . . . . . 9 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 ¬ 𝑧 = 𝐴)
8		nfvd 1919	. . . . . . . . 9 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑧 ¬ 𝑥 = 𝐴)
9		eqeq1 2742	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴))
10	9	a1i 11	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥𝐴 → (𝑧 = 𝑥 → (𝑧 = 𝐴 ↔ 𝑥 = 𝐴)))
11		notbi 318	. . . . . . . . . . 11 ⊢ ((𝑧 = 𝐴 ↔ 𝑥 = 𝐴) ↔ (¬ 𝑧 = 𝐴 ↔ ¬ 𝑥 = 𝐴))
12	10, 11	syl6ib 250	. . . . . . . . . 10 ⊢ (Ⅎ𝑥𝐴 → (𝑧 = 𝑥 → (¬ 𝑧 = 𝐴 ↔ ¬ 𝑥 = 𝐴)))
13		biimp 214	. . . . . . . . . 10 ⊢ ((¬ 𝑧 = 𝐴 ↔ ¬ 𝑥 = 𝐴) → (¬ 𝑧 = 𝐴 → ¬ 𝑥 = 𝐴))
14	12, 13	syl6 35	. . . . . . . . 9 ⊢ (Ⅎ𝑥𝐴 → (𝑧 = 𝑥 → (¬ 𝑧 = 𝐴 → ¬ 𝑥 = 𝐴)))
15	2, 3, 7, 8, 14	cbv1v 2335	. . . . . . . 8 ⊢ (Ⅎ𝑥𝐴 → (∀𝑧 ¬ 𝑧 = 𝐴 → ∀𝑥 ¬ 𝑥 = 𝐴))
16		equcomi 2021	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → 𝑧 = 𝑥)
17		biimpr 219	. . . . . . . . . 10 ⊢ ((¬ 𝑧 = 𝐴 ↔ ¬ 𝑥 = 𝐴) → (¬ 𝑥 = 𝐴 → ¬ 𝑧 = 𝐴))
18	16, 12, 17	syl56 36	. . . . . . . . 9 ⊢ (Ⅎ𝑥𝐴 → (𝑥 = 𝑧 → (¬ 𝑥 = 𝐴 → ¬ 𝑧 = 𝐴)))
19	3, 2, 8, 7, 18	cbv1v 2335	. . . . . . . 8 ⊢ (Ⅎ𝑥𝐴 → (∀𝑥 ¬ 𝑥 = 𝐴 → ∀𝑧 ¬ 𝑧 = 𝐴))
20	15, 19	impbid 211	. . . . . . 7 ⊢ (Ⅎ𝑥𝐴 → (∀𝑧 ¬ 𝑧 = 𝐴 ↔ ∀𝑥 ¬ 𝑥 = 𝐴))
21		alnex 1785	. . . . . . 7 ⊢ (∀𝑧 ¬ 𝑧 = 𝐴 ↔ ¬ ∃𝑧 𝑧 = 𝐴)
22		alnex 1785	. . . . . . 7 ⊢ (∀𝑥 ¬ 𝑥 = 𝐴 ↔ ¬ ∃𝑥 𝑥 = 𝐴)
23	20, 21, 22	3bitr3g 312	. . . . . 6 ⊢ (Ⅎ𝑥𝐴 → (¬ ∃𝑧 𝑧 = 𝐴 ↔ ¬ ∃𝑥 𝑥 = 𝐴))
24	23	con4bid 316	. . . . 5 ⊢ (Ⅎ𝑥𝐴 → (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴))
25	1, 24	syl5ib 243	. . . 4 ⊢ (Ⅎ𝑥𝐴 → (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴))
26	25	ad2antrr 722	. . 3 ⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑)) → (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴))
27	26	3impia 1115	. 2 ⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → ∃𝑥 𝑥 = 𝐴)
28		biimp 214	. . . . . . . . 9 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
29	28	imim2i 16	. . . . . . . 8 ⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝑥 = 𝐴 → (𝜑 → 𝜓)))
30	29	com23 86	. . . . . . 7 ⊢ ((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) → (𝜑 → (𝑥 = 𝐴 → 𝜓)))
31	30	imp 406	. . . . . 6 ⊢ (((𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ 𝜑) → (𝑥 = 𝐴 → 𝜓))
32	31	alanimi 1820	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) → ∀𝑥(𝑥 = 𝐴 → 𝜓))
33		19.23t 2206	. . . . . 6 ⊢ (Ⅎ𝑥𝜓 → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)))
34	33	adantl 481	. . . . 5 ⊢ ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) → (∀𝑥(𝑥 = 𝐴 → 𝜓) ↔ (∃𝑥 𝑥 = 𝐴 → 𝜓)))
35	32, 34	syl5ib 243	. . . 4 ⊢ ((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) → ((∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) → (∃𝑥 𝑥 = 𝐴 → 𝜓)))
36	35	imp 406	. . 3 ⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑)) → (∃𝑥 𝑥 = 𝐴 → 𝜓))
37	36	3adant3 1130	. 2 ⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → (∃𝑥 𝑥 = 𝐴 → 𝜓))
38	27, 37	mpd 15	1 ⊢ (((Ⅎ𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ 𝑉) → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085  ∀wal 1537   = wceq 1539  ∃wex 1783  Ⅎwnf 1787   ∈ wcel 2108  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888

This theorem is referenced by:  vtocldf  3483  bj-vtoclgfALT  35157