Theorem reuop 6282

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 3785	. . 3 ⊢ Ⅎ𝑝[𝑞 / 𝑝]𝜓
2		nfsbc1v 3785	. . 3 ⊢ Ⅎ𝑝[𝑤 / 𝑝]𝜓
3		sbceq1a 3776	. . 3 ⊢ (𝑝 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑝]𝜓))
4		dfsbcq 3767	. . 3 ⊢ (𝑤 = 𝑞 → ([𝑤 / 𝑝]𝜓 ↔ [𝑞 / 𝑝]𝜓))
5	1, 2, 3, 4	reu8nf 3852	. 2 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
6		elxp2 5678	. . . . 5 ⊢ (𝑝 ∈ (𝑋 × 𝑌) ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩)
7		reu3op.a	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜓 ↔ 𝜒))
8	7	biimpcd 249	. . . . . . . . . . . 12 ⊢ (𝜓 → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
9	8	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
10	9	adantr 480	. . . . . . . . . 10 ⊢ (((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
11	10	imp 406	. . . . . . . . 9 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → 𝜒)
12		opelxpi 5691	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
13		dfsbcq 3767	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → ([𝑞 / 𝑝]𝜓 ↔ [⟨𝑥, 𝑦⟩ / 𝑝]𝜓))
14		eqeq2 2747	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → (𝑝 = 𝑞 ↔ 𝑝 = ⟨𝑥, 𝑦⟩))
15	13, 14	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
16	15	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝑞 = ⟨𝑥, 𝑦⟩) → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
17	12, 16	rspcdv 3593	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
18	17	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝜓) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
19		opex 5439	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
20		reuop.x	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜃))
21	19, 20	sbcie 3807	. . . . . . . . . . . . . . . . . . 19 ⊢ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 ↔ 𝜃)
22		pm2.27 42	. . . . . . . . . . . . . . . . . . 19 ⊢ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩))
23	21, 22	sylbir 235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩))
24		eqcom 2742	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ = 𝑝 ↔ 𝑝 = ⟨𝑥, 𝑦⟩)
25	23, 24	imbitrrdi 252	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ = 𝑝))
26	25	com12 32	. . . . . . . . . . . . . . . 16 ⊢ (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → (𝜃 → ⟨𝑥, 𝑦⟩ = 𝑝))
27		eqeq2 2747	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑎, 𝑏⟩ = 𝑝 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = 𝑝))
28	27	eqcoms 2743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = 𝑝))
29	28	imbi2d 340	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ (𝜃 → ⟨𝑥, 𝑦⟩ = 𝑝)))
30	26, 29	syl5ibrcom 247	. . . . . . . . . . . . . . 15 ⊢ (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
31	30	a1d 25	. . . . . . . . . . . . . 14 ⊢ (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
32	18, 31	syl6 35	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝜓) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))))
33	32	expimpd 453	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))))
34	33	imp4c 423	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
35	34	impcom 407	. . . . . . . . . 10 ⊢ (((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
36	35	ralrimivva 3187	. . . . . . . . 9 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
37	11, 36	jca 511	. . . . . . . 8 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
38	37	ex 412	. . . . . . 7 ⊢ (((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
39	38	reximdvva 3192	. . . . . 6 ⊢ ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩ → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
40	39	com12 32	. . . . 5 ⊢ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
41	6, 40	sylbi 217	. . . 4 ⊢ (𝑝 ∈ (𝑋 × 𝑌) → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
42	41	rexlimiv 3134	. . 3 ⊢ (∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
43		opelxpi 5691	. . . . . . 7 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
44	43	adantr 480	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
45		simprl 770	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → 𝜒)
46		nfsbc1v 3785	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥[𝑐 / 𝑥]𝜃
47		nfv 1914	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩
48	46, 47	nfim 1896	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩)
49		nfsbc1v 3785	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦[𝑑 / 𝑦][𝑐 / 𝑥]𝜃
50		nfv 1914	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩
51	49, 50	nfim 1896	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
52		sbceq1a 3776	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → (𝜃 ↔ [𝑐 / 𝑥]𝜃))
53		opeq1 4849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑐 → ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑦⟩)
54	53	eqeq1d 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
55	52, 54	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → ((𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ ([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
56		sbceq1a 3776	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑑 → ([𝑐 / 𝑥]𝜃 ↔ [𝑑 / 𝑦][𝑐 / 𝑥]𝜃))
57		opeq2 4850	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑑 → ⟨𝑐, 𝑦⟩ = ⟨𝑐, 𝑑⟩)
58	57	eqeq1d 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑑 → (⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
59	56, 58	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑑 → (([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
60	48, 51, 55, 59	rspc2 3610	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
61	60	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) ∧ 𝜒) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
62	20	sbcop 5464	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 ↔ [⟨𝑐, 𝑑⟩ / 𝑝]𝜓)
63		pm2.27 42	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
64	62, 63	sylbir 235	. . . . . . . . . . . . . . . . 17 ⊢ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
65		eqcom 2742	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
66	64, 65	imbitrrdi 252	. . . . . . . . . . . . . . . 16 ⊢ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
67	66	com12 32	. . . . . . . . . . . . . . 15 ⊢ (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
68	61, 67	syl6 35	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) ∧ 𝜒) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
69	68	expimpd 453	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
70	69	expcom 413	. . . . . . . . . . . 12 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))))
71	70	impd 410	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
72	71	impcom 407	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
73		dfsbcq 3767	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 ↔ [⟨𝑐, 𝑑⟩ / 𝑝]𝜓))
74		eqeq2 2747	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → (⟨𝑎, 𝑏⟩ = 𝑞 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
75	73, 74	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → (([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞) ↔ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
76	72, 75	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → (𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
77	76	rexlimdvva 3198	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → (∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
78		elxp2 5678	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝑋 × 𝑌) ↔ ∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩)
79	78	biimpi 216	. . . . . . . 8 ⊢ (𝑞 ∈ (𝑋 × 𝑌) → ∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩)
80	77, 79	impel 505	. . . . . . 7 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ 𝑞 ∈ (𝑋 × 𝑌)) → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
81	80	ralrimiva 3132	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
82		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑝𝜒
83		nfcv 2898	. . . . . . . . 9 ⊢ Ⅎ𝑝(𝑋 × 𝑌)
84		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑝⟨𝑎, 𝑏⟩ = 𝑞
85	1, 84	nfim 1896	. . . . . . . . 9 ⊢ Ⅎ𝑝([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)
86	83, 85	nfralw 3291	. . . . . . . 8 ⊢ Ⅎ𝑝∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)
87	82, 86	nfan 1899	. . . . . . 7 ⊢ Ⅎ𝑝(𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
88		eqeq1 2739	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝑝 = 𝑞 ↔ ⟨𝑎, 𝑏⟩ = 𝑞))
89	88	imbi2d 340	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
90	89	ralbidv 3163	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
91	7, 90	anbi12d 632	. . . . . . 7 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ↔ (𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))))
92	87, 91	rspce 3590	. . . . . 6 ⊢ ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌) ∧ (𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
93	44, 45, 81, 92	syl12anc 836	. . . . 5 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
94	93	ex 412	. . . 4 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞))))
95	94	rexlimivv 3186	. . 3 ⊢ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
96	42, 95	impbii 209	. 2 ⊢ (∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
97	5, 96	bitri 275	1 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3051  ∃wrex 3060  ∃!wreu 3357  [wsbc 3765  ⟨cop 4607   × cxp 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-opab 5182  df-xp 5660

This theorem is referenced by:  ichnreuop  47486  ichreuopeq  47487  reuopreuprim  47540