Theorem reuop 6292

Description: There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 23-Jun-2023.)

Hypotheses

Ref	Expression
reu3op.a	⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜓 ↔ 𝜒))
reuop.x	⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
reuop	⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))

Distinct variable groups:   𝑋,𝑎,𝑏,𝑝,𝑥,𝑦   𝑌,𝑎,𝑏,𝑝,𝑥,𝑦   𝜓,𝑎,𝑏,𝑥,𝑦   𝜒,𝑝   𝜃,𝑝

Allowed substitution hints:   𝜓(𝑝)   𝜒(𝑥,𝑦,𝑎,𝑏)   𝜃(𝑥,𝑦,𝑎,𝑏)

Proof of Theorem reuop

Dummy variables 𝑞 𝑐 𝑑 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfsbc1v 3773	. . 3 ⊢ Ⅎ𝑝[𝑞 / 𝑝]𝜓
2		nfsbc1v 3773	. . 3 ⊢ Ⅎ𝑝[𝑤 / 𝑝]𝜓
3		sbceq1a 3764	. . 3 ⊢ (𝑝 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑝]𝜓))
4		dfsbcq 3755	. . 3 ⊢ (𝑤 = 𝑞 → ([𝑤 / 𝑝]𝜓 ↔ [𝑞 / 𝑝]𝜓))
5	1, 2, 3, 4	reu8nf 3839	. 2 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
6		elxp2 5683	. . . . 5 ⊢ (𝑝 ∈ (𝑋 × 𝑌) ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩)
7		reu3op.a	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜓 ↔ 𝜒))
8	7	biimpcd 252	. . . . . . . . . . . 12 ⊢ (𝜓 → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
9	8	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
10	9	adantr 485	. . . . . . . . . 10 ⊢ (((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
11	10	imp 411	. . . . . . . . 9 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → 𝜒)
12		opelxpi 5696	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
13		dfsbcq 3755	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → ([𝑞 / 𝑝]𝜓 ↔ [⟨𝑥, 𝑦⟩ / 𝑝]𝜓))
14		eqeq2 2781	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → (𝑝 = 𝑞 ↔ 𝑝 = ⟨𝑥, 𝑦⟩))
15	13, 14	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
16	15	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝑞 = ⟨𝑥, 𝑦⟩) → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
17	12, 16	rspcdv 3582	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
18	17	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝜓) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
19		opex 5443	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
20		reuop.x	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜃))
21	19, 20	sbcie 3794	. . . . . . . . . . . . . . . . . . 19 ⊢ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 ↔ 𝜃)
22		pm2.27 43	. . . . . . . . . . . . . . . . . . 19 ⊢ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩))
23	21, 22	sylbir 238	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩))
24		eqcom 2776	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ = 𝑝 ↔ 𝑝 = ⟨𝑥, 𝑦⟩)
25	23, 24	imbitrrdi 255	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ = 𝑝))
26	25	com12 33	. . . . . . . . . . . . . . . 16 ⊢ (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → (𝜃 → ⟨𝑥, 𝑦⟩ = 𝑝))
27		eqeq2 2781	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑎, 𝑏⟩ = 𝑝 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = 𝑝))
28	27	eqcoms 2777	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = 𝑝))
29	28	imbi2d 343	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ (𝜃 → ⟨𝑥, 𝑦⟩ = 𝑝)))
30	26, 29	syl5ibrcom 250	. . . . . . . . . . . . . . 15 ⊢ (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
31	30	a1d 26	. . . . . . . . . . . . . 14 ⊢ (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
32	18, 31	syl6 36	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝜓) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))))
33	32	expimpd 458	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))))
34	33	imp4c 428	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
35	34	impcom 412	. . . . . . . . . 10 ⊢ (((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
36	35	ralrimivva 3214	. . . . . . . . 9 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
37	11, 36	jca 520	. . . . . . . 8 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
38	37	ex 417	. . . . . . 7 ⊢ (((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
39	38	reximdvva 3219	. . . . . 6 ⊢ ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩ → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
40	39	com12 33	. . . . 5 ⊢ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
41	6, 40	sylbi 220	. . . 4 ⊢ (𝑝 ∈ (𝑋 × 𝑌) → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
42	41	rexlimiv 3165	. . 3 ⊢ (∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
43		opelxpi 5696	. . . . . . 7 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
44	43	adantr 485	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
45		simprl 782	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → 𝜒)
46		nfsbc1v 3773	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥[𝑐 / 𝑥]𝜃
47		nfv 1941	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩
48	46, 47	nfim 1923	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩)
49		nfsbc1v 3773	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦[𝑑 / 𝑦][𝑐 / 𝑥]𝜃
50		nfv 1941	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩
51	49, 50	nfim 1923	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
52		sbceq1a 3764	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → (𝜃 ↔ [𝑐 / 𝑥]𝜃))
53		opeq1 4839	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑐 → ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑦⟩)
54	53	eqeq1d 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
55	52, 54	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → ((𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ ([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
56		sbceq1a 3764	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑑 → ([𝑐 / 𝑥]𝜃 ↔ [𝑑 / 𝑦][𝑐 / 𝑥]𝜃))
57		opeq2 4840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑑 → ⟨𝑐, 𝑦⟩ = ⟨𝑐, 𝑑⟩)
58	57	eqeq1d 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑑 → (⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
59	56, 58	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑑 → (([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
60	48, 51, 55, 59	rspc2 3599	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
61	60	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) ∧ 𝜒) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
62	20	sbcop 5469	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 ↔ [⟨𝑐, 𝑑⟩ / 𝑝]𝜓)
63		pm2.27 43	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
64	62, 63	sylbir 238	. . . . . . . . . . . . . . . . 17 ⊢ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
65		eqcom 2776	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
66	64, 65	imbitrrdi 255	. . . . . . . . . . . . . . . 16 ⊢ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
67	66	com12 33	. . . . . . . . . . . . . . 15 ⊢ (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
68	61, 67	syl6 36	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) ∧ 𝜒) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
69	68	expimpd 458	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
70	69	expcom 418	. . . . . . . . . . . 12 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))))
71	70	impd 415	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
72	71	impcom 412	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
73		dfsbcq 3755	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 ↔ [⟨𝑐, 𝑑⟩ / 𝑝]𝜓))
74		eqeq2 2781	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → (⟨𝑎, 𝑏⟩ = 𝑞 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
75	73, 74	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → (([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞) ↔ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
76	72, 75	syl5ibrcom 250	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → (𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
77	76	rexlimdvva 3228	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → (∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
78		elxp2 5683	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝑋 × 𝑌) ↔ ∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩)
79	78	biimpi 219	. . . . . . . 8 ⊢ (𝑞 ∈ (𝑋 × 𝑌) → ∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩)
80	77, 79	impel 514	. . . . . . 7 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ 𝑞 ∈ (𝑋 × 𝑌)) → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
81	80	ralrimiva 3163	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
82		nfv 1941	. . . . . . . 8 ⊢ Ⅎ𝑝𝜒
83		nfcv 2931	. . . . . . . . 9 ⊢ Ⅎ𝑝(𝑋 × 𝑌)
84		nfv 1941	. . . . . . . . . 10 ⊢ Ⅎ𝑝⟨𝑎, 𝑏⟩ = 𝑞
85	1, 84	nfim 1923	. . . . . . . . 9 ⊢ Ⅎ𝑝([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)
86	83, 85	nfralw 3318	. . . . . . . 8 ⊢ Ⅎ𝑝∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)
87	82, 86	nfan 1926	. . . . . . 7 ⊢ Ⅎ𝑝(𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
88		eqeq1 2773	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝑝 = 𝑞 ↔ ⟨𝑎, 𝑏⟩ = 𝑞))
89	88	imbi2d 343	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
90	89	ralbidv 3194	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
91	7, 90	anbi12d 643	. . . . . . 7 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ↔ (𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))))
92	87, 91	rspce 3579	. . . . . 6 ⊢ ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌) ∧ (𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
93	44, 45, 81, 92	syl12anc 849	. . . . 5 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
94	93	ex 417	. . . 4 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞))))
95	94	rexlimivv 3213	. . 3 ⊢ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
96	42, 95	impbii 212	. 2 ⊢ (∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
97	5, 96	bitri 278	1 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  ∃!wreu 3374  [wsbc 3753  ⟨cop 4597   × cxp 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5175  df-xp 5665

This theorem is referenced by:  ichnreuop  48105  ichreuopeq  48106  reuopreuprim  48159