Theorem oprabidw 7306

Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of oprabid 7307 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 20-Mar-2013.) (Revised by Gino Giotto, 26-Jan-2024.)

Assertion

Ref	Expression
oprabidw	⊢ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)

Distinct variable group:   𝑥,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem oprabidw

Dummy variables 𝑎 𝑟 𝑠 𝑡 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opex 5379	. 2 ⊢ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ V
2		opex 5379	. . . . . 6 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
3		vex 3436	. . . . . 6 ⊢ 𝑧 ∈ V
4	2, 3	eqvinop 5401	. . . . 5 ⊢ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ∃𝑎∃𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
5	4	biimpi 215	. . . 4 ⊢ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ∃𝑎∃𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
6		eqeq1 2742	. . . . . . . 8 ⊢ (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
7		vex 3436	. . . . . . . . 9 ⊢ 𝑎 ∈ V
8		vex 3436	. . . . . . . . 9 ⊢ 𝑡 ∈ V
9	7, 8	opth1 5390	. . . . . . . 8 ⊢ (⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩)
10	6, 9	syl6bi 252	. . . . . . 7 ⊢ (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → 𝑎 = ⟨𝑥, 𝑦⟩))
11		vex 3436	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
12		vex 3436	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
13	11, 12	eqvinop 5401	. . . . . . . . 9 ⊢ (𝑎 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑟∃𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩))
14		opeq1 4804	. . . . . . . . . . . . 13 ⊢ (𝑎 = ⟨𝑟, 𝑠⟩ → ⟨𝑎, 𝑡⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
15	14	eqeq2d 2749	. . . . . . . . . . . 12 ⊢ (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ ↔ 𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
16	11, 12, 3	otth2 5398	. . . . . . . . . . . . . . 15 ⊢ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ (𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡))
17		euequ 2597	. . . . . . . . . . . . . . . . . 18 ⊢ ∃!𝑥 𝑥 = 𝑟
18		eupick 2635	. . . . . . . . . . . . . . . . . 18 ⊢ ((∃!𝑥 𝑥 = 𝑟 ∧ ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))))
19	17, 18	mpan 687	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))))
20		euequ 2597	. . . . . . . . . . . . . . . . . . 19 ⊢ ∃!𝑦 𝑦 = 𝑠
21		eupick 2635	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃!𝑦 𝑦 = 𝑠 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))
22	20, 21	mpan 687	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 → ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))
23		euequ 2597	. . . . . . . . . . . . . . . . . . 19 ⊢ ∃!𝑧 𝑧 = 𝑡
24		eupick 2635	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∃!𝑧 𝑧 = 𝑡 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑧 = 𝑡 → 𝜑))
25	23, 24	mpan 687	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑧(𝑧 = 𝑡 ∧ 𝜑) → (𝑧 = 𝑡 → 𝜑))
26	22, 25	syl6 35	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 → (𝑧 = 𝑡 → 𝜑)))
27	19, 26	syl6 35	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 → (𝑦 = 𝑠 → (𝑧 = 𝑡 → 𝜑))))
28	27	3impd 1347	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡) → 𝜑))
29	16, 28	syl5bi 241	. . . . . . . . . . . . . 14 ⊢ (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))) → (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → 𝜑))
30		df-3an 1088	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡) ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡))
31	16, 30	bitri 274	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡))
32	31	anbi1i 624	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑))
33		anass 469	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ 𝑧 = 𝑡) ∧ 𝜑) ↔ ((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ (𝑧 = 𝑡 ∧ 𝜑)))
34		anass 469	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 = 𝑟 ∧ 𝑦 = 𝑠) ∧ (𝑧 = 𝑡 ∧ 𝜑)) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
35	32, 33, 34	3bitri 297	. . . . . . . . . . . . . . . 16 ⊢ ((⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ (𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
36	35	3exbii 1852	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥∃𝑦∃𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
37		nfe1 2147	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑥∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))
38		19.8a 2174	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))
39	38	anim2i 617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
40	39	eximi 1837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑧(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
41		biidd 261	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ (𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))))
42	41	drex1v 2369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 𝑥 = 𝑧 → (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑧(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))))
43	40, 42	syl5ibr 245	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑥 𝑥 = 𝑧 → (∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))))
44		19.40 1889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (∃𝑧 𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
45		nfvd 1918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧 𝑥 = 𝑟)
46	45	19.9d 2196	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (∃𝑧 𝑥 = 𝑟 → 𝑥 = 𝑟))
47	46	anim1d 611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ((∃𝑧 𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))))
48		19.8a 2174	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
49	44, 47, 48	syl56 36	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))))
50	43, 49	pm2.61i 182	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
51	37, 50	exlimi 2210	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
52	51	eximi 1837	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑦∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
53		excom 2162	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑦∃𝑥∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
54		excom 2162	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑦∃𝑥(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
55	52, 53, 54	3imtr4i 292	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
56		nfe1 2147	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))
57		19.8a 2174	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))
58	57	anim2i 617	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
59	58	eximi 1837	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑦(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
60		biidd 261	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑥 𝑥 = 𝑦 → ((𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ (𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))))
61	60	drex1v 2369	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) ↔ ∃𝑦(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))))
62	59, 61	syl5ibr 245	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))))
63		19.40 1889	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (∃𝑦 𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
64		nfvd 1918	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑟)
65	64	19.9d 2196	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑦 𝑥 = 𝑟 → 𝑥 = 𝑟))
66	65	anim1d 611	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ((∃𝑦 𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))))
67		19.8a 2174	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
68	63, 66, 67	syl56 36	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)))))
69	62, 68	pm2.61i 182	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
70	56, 69	exlimi 2210	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑟 ∧ ∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))))
71		nfe1 2147	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑦∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))
72		19.8a 2174	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 = 𝑡 ∧ 𝜑) → ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))
73	72	anim2i 617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))
74	73	eximi 1837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑧(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))
75		biidd 261	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 𝑦 = 𝑧 → ((𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) ↔ (𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))))
76	75	drex1v 2369	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 𝑦 = 𝑧 → (∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) ↔ ∃𝑧(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))))
77	74, 76	syl5ibr 245	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑦 𝑦 = 𝑧 → (∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))))
78		19.40 1889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → (∃𝑧 𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))
79		nfvd 1918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑦 = 𝑠)
80	79	19.9d 2196	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∃𝑧 𝑦 = 𝑠 → 𝑦 = 𝑠))
81	80	anim1d 611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ((∃𝑧 𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → (𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))))
82		19.8a 2174	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))
83	78, 81, 82	syl56 36	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))))
84	77, 83	pm2.61i 182	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))
85	71, 84	exlimi 2210	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑)) → ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑)))
86	85	anim2i 617	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → (𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))))
87	86	eximi 1837	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦∃𝑧(𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))))
88	55, 70, 87	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥∃𝑦∃𝑧(𝑥 = 𝑟 ∧ (𝑦 = 𝑠 ∧ (𝑧 = 𝑡 ∧ 𝜑))) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))))
89	36, 88	sylbi 216	. . . . . . . . . . . . . 14 ⊢ (∃𝑥∃𝑦∃𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → ∃𝑥(𝑥 = 𝑟 ∧ ∃𝑦(𝑦 = 𝑠 ∧ ∃𝑧(𝑧 = 𝑡 ∧ 𝜑))))
90	29, 89	syl11 33	. . . . . . . . . . . . 13 ⊢ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥∃𝑦∃𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))
91		eqeq1 2742	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
92		eqcom 2745	. . . . . . . . . . . . . . 15 ⊢ (⟨⟨𝑟, 𝑠⟩, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩)
93	91, 92	bitrdi 287	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩))
94	93	anbi1d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑)))
95	94	3exbidv 1928	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦∃𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑)))
96	95	imbi1d 342	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑) ↔ (∃𝑥∃𝑦∃𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑)))
97	93, 96	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)) ↔ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (∃𝑥∃𝑦∃𝑧(⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ ∧ 𝜑) → 𝜑))))
98	90, 97	mpbiri 257	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨⟨𝑟, 𝑠⟩, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
99	15, 98	syl6bi 252	. . . . . . . . . . 11 ⊢ (𝑎 = ⟨𝑟, 𝑠⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
100	99	adantr 481	. . . . . . . . . 10 ⊢ ((𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
101	100	exlimivv 1935	. . . . . . . . 9 ⊢ (∃𝑟∃𝑠(𝑎 = ⟨𝑟, 𝑠⟩ ∧ ⟨𝑟, 𝑠⟩ = ⟨𝑥, 𝑦⟩) → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
102	13, 101	sylbi 216	. . . . . . . 8 ⊢ (𝑎 = ⟨𝑥, 𝑦⟩ → (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
103	102	com3l 89	. . . . . . 7 ⊢ (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝑎 = ⟨𝑥, 𝑦⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))))
104	10, 103	mpdd 43	. . . . . 6 ⊢ (𝑤 = ⟨𝑎, 𝑡⟩ → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
105	104	adantr 481	. . . . 5 ⊢ ((𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
106	105	exlimivv 1935	. . . 4 ⊢ (∃𝑎∃𝑡(𝑤 = ⟨𝑎, 𝑡⟩ ∧ ⟨𝑎, 𝑡⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑)))
107	5, 106	mpcom 38	. . 3 ⊢ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → 𝜑))
108		19.8a 2174	. . . . 5 ⊢ ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
109		19.8a 2174	. . . . 5 ⊢ (∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
110		19.8a 2174	. . . . 5 ⊢ (∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
111	108, 109, 110	3syl 18	. . . 4 ⊢ ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) → ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
112	111	ex 413	. . 3 ⊢ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (𝜑 → ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)))
113	107, 112	impbid 211	. 2 ⊢ (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ 𝜑))
114		df-oprab 7279	. 2 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥∃𝑦∃𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
115	1, 113, 114	elab2 3613	1 ⊢ (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2106  ∃!weu 2568  ⟨cop 4567  {coprab 7276

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  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-oprab 7279

This theorem is referenced by:  eqoprab2bw  7345  ovid  7414  ovidig  7415  tposoprab  8078  xpcomco  8849