Theorem opreu2reuALT 31705

Description: Correspondence between uniqueness of ordered pairs and double restricted existential uniqueness quantification. Alternate proof of one direction only, use opreu2reurex 6291 instead. (Contributed by Thierry Arnoux, 4-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
opsbc2ie.a	⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))

Assertion

Ref	Expression
opreu2reuALT	⊢ ((∃!𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ ∃!𝑏 ∈ 𝐵 ∃𝑎 ∈ 𝐴 𝜒) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)

Distinct variable groups:   𝑎,𝑏,𝑝   𝜑,𝑎,𝑏   𝐴,𝑎,𝑏,𝑝   𝐵,𝑎,𝑏,𝑝   𝜒,𝑎,𝑏,𝑝

Allowed substitution hint:   𝜑(𝑝)

Proof of Theorem opreu2reuALT

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2reu4 4526	. 2 ⊢ ((∃!𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ ∃!𝑏 ∈ 𝐵 ∃𝑎 ∈ 𝐴 𝜒) ↔ (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))))
2		simpllr 775	. . . . . 6 ⊢ ((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) → 𝑥 ∈ 𝐴)
3		simplr 768	. . . . . 6 ⊢ ((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) → 𝑦 ∈ 𝐵)
4		opelxpi 5713	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵))
5	2, 3, 4	syl2anc 585	. . . . 5 ⊢ ((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵))
6		nfre1 3283	. . . . . . . . 9 ⊢ Ⅎ𝑎∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒
7		nfv 1918	. . . . . . . . 9 ⊢ Ⅎ𝑎 𝑥 ∈ 𝐴
8	6, 7	nfan 1903	. . . . . . . 8 ⊢ Ⅎ𝑎(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴)
9		nfv 1918	. . . . . . . 8 ⊢ Ⅎ𝑎 𝑦 ∈ 𝐵
10	8, 9	nfan 1903	. . . . . . 7 ⊢ Ⅎ𝑎((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)
11		nfra1 3282	. . . . . . 7 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
12	10, 11	nfan 1903	. . . . . 6 ⊢ Ⅎ𝑎(((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
13		nfcv 2904	. . . . . . 7 ⊢ Ⅎ𝑎𝑦
14		nfsbc1v 3797	. . . . . . 7 ⊢ Ⅎ𝑎[𝑥 / 𝑎]𝜒
15	13, 14	nfsbc 3802	. . . . . 6 ⊢ Ⅎ𝑎[𝑦 / 𝑏][𝑥 / 𝑎]𝜒
16		nfcv 2904	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏𝐴
17		nfre1 3283	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐵 𝜒
18	16, 17	nfrexw 3311	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒
19		nfv 1918	. . . . . . . . . . . 12 ⊢ Ⅎ𝑏 𝑥 ∈ 𝐴
20	18, 19	nfan 1903	. . . . . . . . . . 11 ⊢ Ⅎ𝑏(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴)
21		nfv 1918	. . . . . . . . . . 11 ⊢ Ⅎ𝑏 𝑦 ∈ 𝐵
22	20, 21	nfan 1903	. . . . . . . . . 10 ⊢ Ⅎ𝑏((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)
23		nfcv 2904	. . . . . . . . . . 11 ⊢ Ⅎ𝑏𝐴
24		nfra1 3282	. . . . . . . . . . 11 ⊢ Ⅎ𝑏∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
25	23, 24	nfral 3371	. . . . . . . . . 10 ⊢ Ⅎ𝑏∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
26	22, 25	nfan 1903	. . . . . . . . 9 ⊢ Ⅎ𝑏(((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
27		nfv 1918	. . . . . . . . 9 ⊢ Ⅎ𝑏 𝑎 ∈ 𝐴
28	26, 27	nfan 1903	. . . . . . . 8 ⊢ Ⅎ𝑏((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴)
29		nfre1 3283	. . . . . . . 8 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐵 𝜒
30	28, 29	nfan 1903	. . . . . . 7 ⊢ Ⅎ𝑏(((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ ∃𝑏 ∈ 𝐵 𝜒)
31		nfsbc1v 3797	. . . . . . 7 ⊢ Ⅎ𝑏[𝑦 / 𝑏][𝑥 / 𝑎]𝜒
32		rspa 3246	. . . . . . . . . . . 12 ⊢ ((∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)) ∧ 𝑎 ∈ 𝐴) → ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
33	32	ad5ant23 759	. . . . . . . . . . 11 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
34		simplr 768	. . . . . . . . . . 11 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → 𝑏 ∈ 𝐵)
35		simpr 486	. . . . . . . . . . 11 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → 𝜒)
36		rspa 3246	. . . . . . . . . . . 12 ⊢ ((∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)) ∧ 𝑏 ∈ 𝐵) → (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
37	36	imp 408	. . . . . . . . . . 11 ⊢ (((∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
38	33, 34, 35, 37	syl21anc 837	. . . . . . . . . 10 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
39	38	simprd 497	. . . . . . . . 9 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → 𝑏 = 𝑦)
40		rspa 3246	. . . . . . . . . . . . 13 ⊢ ((∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)) ∧ 𝑎 ∈ 𝐴) → ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
41	40	ad5ant23 759	. . . . . . . . . . . 12 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
42		simplr 768	. . . . . . . . . . . 12 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → 𝑏 ∈ 𝐵)
43		simpr 486	. . . . . . . . . . . 12 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → 𝜒)
44		rspa 3246	. . . . . . . . . . . . 13 ⊢ ((∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)) ∧ 𝑏 ∈ 𝐵) → (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
45	44	imp 408	. . . . . . . . . . . 12 ⊢ (((∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
46	41, 42, 43, 45	syl21anc 837	. . . . . . . . . . 11 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
47	46	simpld 496	. . . . . . . . . 10 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → 𝑎 = 𝑥)
48		simpr 486	. . . . . . . . . 10 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → 𝜒)
49		sbceq1a 3788	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑥 → (𝜒 ↔ [𝑥 / 𝑎]𝜒))
50	49	biimpa 478	. . . . . . . . . 10 ⊢ ((𝑎 = 𝑥 ∧ 𝜒) → [𝑥 / 𝑎]𝜒)
51	47, 48, 50	syl2anc 585	. . . . . . . . 9 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → [𝑥 / 𝑎]𝜒)
52		sbceq1a 3788	. . . . . . . . . 10 ⊢ (𝑏 = 𝑦 → ([𝑥 / 𝑎]𝜒 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒))
53	52	biimpa 478	. . . . . . . . 9 ⊢ ((𝑏 = 𝑦 ∧ [𝑥 / 𝑎]𝜒) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
54	39, 51, 53	syl2anc 585	. . . . . . . 8 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
55	54	adantllr 718	. . . . . . 7 ⊢ ((((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ ∃𝑏 ∈ 𝐵 𝜒) ∧ 𝑏 ∈ 𝐵) ∧ 𝜒) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
56		simpr 486	. . . . . . 7 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ ∃𝑏 ∈ 𝐵 𝜒) → ∃𝑏 ∈ 𝐵 𝜒)
57	30, 31, 55, 56	r19.29af2 3265	. . . . . 6 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑎 ∈ 𝐴) ∧ ∃𝑏 ∈ 𝐵 𝜒) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
58		simplll 774	. . . . . 6 ⊢ ((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒)
59	12, 15, 57, 58	r19.29af2 3265	. . . . 5 ⊢ ((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
60		1st2nd2 8011	. . . . . . . . 9 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → 𝑝 = ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩)
61	60	ad2antlr 726	. . . . . . . 8 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → 𝑝 = ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩)
62		nfre1 3283	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒
63		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎 𝑥 ∈ 𝐴
64	62, 63	nfan 1903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴)
65		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎 𝑦 ∈ 𝐵
66	64, 65	nfan 1903	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑎((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)
67		nfra1 3282	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
68	66, 67	nfan 1903	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑎(((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
69		nfv 1918	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑎 𝑝 ∈ (𝐴 × 𝐵)
70	68, 69	nfan 1903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑎((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵))
71		nfv 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑎𝜑
72	70, 71	nfan 1903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑎(((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑)
73		nfcv 2904	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑏𝐴
74		nfre1 3283	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐵 𝜒
75	73, 74	nfrexw 3311	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑏∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒
76		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑏 𝑥 ∈ 𝐴
77	75, 76	nfan 1903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴)
78		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏 𝑦 ∈ 𝐵
79	77, 78	nfan 1903	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)
80		nfcv 2904	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏𝐴
81		nfra1 3282	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
82	80, 81	nfral 3371	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
83	79, 82	nfan 1903	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏(((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
84		nfv 1918	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏 𝑝 ∈ (𝐴 × 𝐵)
85	83, 84	nfan 1903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵))
86		nfv 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏𝜑
87	85, 86	nfan 1903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏(((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑)
88		nfv 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑎(𝜑 → ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦))
89		nfv 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏(𝜑 → ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦))
90		xp1st 8004	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → (1st ‘𝑝) ∈ 𝐴)
91	90	ad2antlr 726	. . . . . . . . . . . . 13 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (1st ‘𝑝) ∈ 𝐴)
92		xp2nd 8005	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → (2nd ‘𝑝) ∈ 𝐵)
93	92	ad2antlr 726	. . . . . . . . . . . . 13 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (2nd ‘𝑝) ∈ 𝐵)
94		eqcom 2740	. . . . . . . . . . . . . . . . 17 ⊢ ((1st ‘𝑝) = 𝑎 ↔ 𝑎 = (1st ‘𝑝))
95		eqcom 2740	. . . . . . . . . . . . . . . . 17 ⊢ ((2nd ‘𝑝) = 𝑏 ↔ 𝑏 = (2nd ‘𝑝))
96		eqopi 8008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st ‘𝑝) = 𝑎 ∧ (2nd ‘𝑝) = 𝑏)) → 𝑝 = ⟨𝑎, 𝑏⟩)
97		opsbc2ie.a	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))
98	96, 97	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st ‘𝑝) = 𝑎 ∧ (2nd ‘𝑝) = 𝑏)) → (𝜑 ↔ 𝜒))
99	98	bicomd 222	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st ‘𝑝) = 𝑎 ∧ (2nd ‘𝑝) = 𝑏)) → (𝜒 ↔ 𝜑))
100	99	ancoms 460	. . . . . . . . . . . . . . . . . 18 ⊢ ((((1st ‘𝑝) = 𝑎 ∧ (2nd ‘𝑝) = 𝑏) ∧ 𝑝 ∈ (𝐴 × 𝐵)) → (𝜒 ↔ 𝜑))
101	100	ex 414	. . . . . . . . . . . . . . . . 17 ⊢ (((1st ‘𝑝) = 𝑎 ∧ (2nd ‘𝑝) = 𝑏) → (𝑝 ∈ (𝐴 × 𝐵) → (𝜒 ↔ 𝜑)))
102	94, 95, 101	syl2anbr 600	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → (𝑝 ∈ (𝐴 × 𝐵) → (𝜒 ↔ 𝜑)))
103	102	impcom 409	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ (𝐴 × 𝐵) ∧ (𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝))) → (𝜒 ↔ 𝜑))
104	103	ad4ant24 753	. . . . . . . . . . . . . 14 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝))) → (𝜒 ↔ 𝜑))
105		simpl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → 𝑎 = (1st ‘𝑝))
106	105	eqeq1d 2735	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → (𝑎 = 𝑥 ↔ (1st ‘𝑝) = 𝑥))
107		simpr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → 𝑏 = (2nd ‘𝑝))
108	107	eqeq1d 2735	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → (𝑏 = 𝑦 ↔ (2nd ‘𝑝) = 𝑦))
109	106, 108	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) ↔ ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦)))
110	109	adantl 483	. . . . . . . . . . . . . 14 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝))) → ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) ↔ ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦)))
111	104, 110	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝))) → ((𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)) ↔ (𝜑 → ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦))))
112		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
113	72, 87, 88, 89, 91, 93, 111, 112	rspc2daf 31696	. . . . . . . . . . . 12 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (𝜑 → ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦)))
114	113	com12 32	. . . . . . . . . . 11 ⊢ (𝜑 → ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦)))
115	114	anabsi7 670	. . . . . . . . . 10 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦))
116	115	simpld 496	. . . . . . . . 9 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (1st ‘𝑝) = 𝑥)
117		nfre1 3283	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒
118		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑎 𝑥 ∈ 𝐴
119	117, 118	nfan 1903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴)
120		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑎 𝑦 ∈ 𝐵
121	119, 120	nfan 1903	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑎((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)
122		nfra1 3282	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
123	121, 122	nfan 1903	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑎(((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
124		nfv 1918	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑎 𝑝 ∈ (𝐴 × 𝐵)
125	123, 124	nfan 1903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑎((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵))
126		nfv 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑎𝜑
127	125, 126	nfan 1903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑎(((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑)
128		nfcv 2904	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑏𝐴
129		nfre1 3283	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑏∃𝑏 ∈ 𝐵 𝜒
130	128, 129	nfrexw 3311	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑏∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒
131		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑏 𝑥 ∈ 𝐴
132	130, 131	nfan 1903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏(∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴)
133		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏 𝑦 ∈ 𝐵
134	132, 133	nfan 1903	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)
135		nfcv 2904	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏𝐴
136		nfra1 3282	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑏∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
137	135, 136	nfral 3371	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑏∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))
138	134, 137	nfan 1903	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏(((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
139		nfv 1918	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑏 𝑝 ∈ (𝐴 × 𝐵)
140	138, 139	nfan 1903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵))
141		nfv 1918	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑏𝜑
142	140, 141	nfan 1903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏(((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑)
143		nfv 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑎(𝜑 → ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦))
144		nfv 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑏(𝜑 → ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦))
145		xp1st 8004	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → (1st ‘𝑝) ∈ 𝐴)
146	145	ad2antlr 726	. . . . . . . . . . . . 13 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (1st ‘𝑝) ∈ 𝐴)
147		xp2nd 8005	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → (2nd ‘𝑝) ∈ 𝐵)
148	147	ad2antlr 726	. . . . . . . . . . . . 13 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (2nd ‘𝑝) ∈ 𝐵)
149		eqcom 2740	. . . . . . . . . . . . . . . . 17 ⊢ ((1st ‘𝑝) = 𝑎 ↔ 𝑎 = (1st ‘𝑝))
150		eqcom 2740	. . . . . . . . . . . . . . . . 17 ⊢ ((2nd ‘𝑝) = 𝑏 ↔ 𝑏 = (2nd ‘𝑝))
151		eqopi 8008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st ‘𝑝) = 𝑎 ∧ (2nd ‘𝑝) = 𝑏)) → 𝑝 = ⟨𝑎, 𝑏⟩)
152	151, 97	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st ‘𝑝) = 𝑎 ∧ (2nd ‘𝑝) = 𝑏)) → (𝜑 ↔ 𝜒))
153	152	bicomd 222	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st ‘𝑝) = 𝑎 ∧ (2nd ‘𝑝) = 𝑏)) → (𝜒 ↔ 𝜑))
154	153	ancoms 460	. . . . . . . . . . . . . . . . . 18 ⊢ ((((1st ‘𝑝) = 𝑎 ∧ (2nd ‘𝑝) = 𝑏) ∧ 𝑝 ∈ (𝐴 × 𝐵)) → (𝜒 ↔ 𝜑))
155	154	ex 414	. . . . . . . . . . . . . . . . 17 ⊢ (((1st ‘𝑝) = 𝑎 ∧ (2nd ‘𝑝) = 𝑏) → (𝑝 ∈ (𝐴 × 𝐵) → (𝜒 ↔ 𝜑)))
156	149, 150, 155	syl2anbr 600	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → (𝑝 ∈ (𝐴 × 𝐵) → (𝜒 ↔ 𝜑)))
157	156	impcom 409	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ (𝐴 × 𝐵) ∧ (𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝))) → (𝜒 ↔ 𝜑))
158	157	ad4ant24 753	. . . . . . . . . . . . . 14 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝))) → (𝜒 ↔ 𝜑))
159		simpl 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → 𝑎 = (1st ‘𝑝))
160	159	eqeq1d 2735	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → (𝑎 = 𝑥 ↔ (1st ‘𝑝) = 𝑥))
161		simpr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → 𝑏 = (2nd ‘𝑝))
162	161	eqeq1d 2735	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → (𝑏 = 𝑦 ↔ (2nd ‘𝑝) = 𝑦))
163	160, 162	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) ↔ ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦)))
164	163	adantl 483	. . . . . . . . . . . . . 14 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝))) → ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) ↔ ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦)))
165	158, 164	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝))) → ((𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)) ↔ (𝜑 → ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦))))
166		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦)))
167	127, 142, 143, 144, 146, 148, 165, 166	rspc2daf 31696	. . . . . . . . . . . 12 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (𝜑 → ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦)))
168	167	com12 32	. . . . . . . . . . 11 ⊢ (𝜑 → ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦)))
169	168	anabsi7 670	. . . . . . . . . 10 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ((1st ‘𝑝) = 𝑥 ∧ (2nd ‘𝑝) = 𝑦))
170	169	simprd 497	. . . . . . . . 9 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (2nd ‘𝑝) = 𝑦)
171	116, 170	opeq12d 4881	. . . . . . . 8 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ = ⟨𝑥, 𝑦⟩)
172	61, 171	eqtrd 2773	. . . . . . 7 ⊢ ((((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → 𝑝 = ⟨𝑥, 𝑦⟩)
173	172	ex 414	. . . . . 6 ⊢ (((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) → (𝜑 → 𝑝 = ⟨𝑥, 𝑦⟩))
174	173	ralrimiva 3147	. . . . 5 ⊢ ((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) → ∀𝑝 ∈ (𝐴 × 𝐵)(𝜑 → 𝑝 = ⟨𝑥, 𝑦⟩))
175	5, 59, 174	3jca 1129	. . . 4 ⊢ ((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) → (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒 ∧ ∀𝑝 ∈ (𝐴 × 𝐵)(𝜑 → 𝑝 = ⟨𝑥, 𝑦⟩)))
176	97	opsbc2ie 31704	. . . . 5 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒))
177	176	eqreu 3725	. . . 4 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒 ∧ ∀𝑝 ∈ (𝐴 × 𝐵)(𝜑 → 𝑝 = ⟨𝑥, 𝑦⟩)) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
178	175, 177	syl 17	. . 3 ⊢ ((((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
179	178	r19.29ffa 31701	. 2 ⊢ ((∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 (𝜒 → (𝑎 = 𝑥 ∧ 𝑏 = 𝑦))) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
180	1, 179	sylbi 216	1 ⊢ ((∃!𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ ∃!𝑏 ∈ 𝐵 ∃𝑎 ∈ 𝐴 𝜒) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071  ∃!wreu 3375  [wsbc 3777  ⟨cop 4634   × cxp 5674  ‘cfv 6541  1^st c1st 7970  2^nd c2nd 7971

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-13 2372  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6493  df-fun 6543  df-fv 6549  df-1st 7972  df-2nd 7973

This theorem is referenced by: (None)