Theorem reuop 6144

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 3792	. . 3 ⊢ Ⅎ𝑝[𝑞 / 𝑝]𝜓
2		nfsbc1v 3792	. . 3 ⊢ Ⅎ𝑝[𝑤 / 𝑝]𝜓
3		sbceq1a 3783	. . 3 ⊢ (𝑝 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑝]𝜓))
4		dfsbcq 3774	. . 3 ⊢ (𝑤 = 𝑞 → ([𝑤 / 𝑝]𝜓 ↔ [𝑞 / 𝑝]𝜓))
5	1, 2, 3, 4	reu8nf 3860	. 2 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
6		elxp2 5579	. . . . 5 ⊢ (𝑝 ∈ (𝑋 × 𝑌) ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩)
7		reu3op.a	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜓 ↔ 𝜒))
8	7	biimpcd 251	. . . . . . . . . . . 12 ⊢ (𝜓 → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
9	8	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
10	9	adantr 483	. . . . . . . . . 10 ⊢ (((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
11	10	imp 409	. . . . . . . . 9 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → 𝜒)
12		opelxpi 5592	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
13		dfsbcq 3774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → ([𝑞 / 𝑝]𝜓 ↔ [⟨𝑥, 𝑦⟩ / 𝑝]𝜓))
14		eqeq2 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → (𝑝 = 𝑞 ↔ 𝑝 = ⟨𝑥, 𝑦⟩))
15	13, 14	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
16	15	adantl 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝑞 = ⟨𝑥, 𝑦⟩) → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
17	12, 16	rspcdv 3615	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
18	17	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝜓) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
19		opex 5356	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
20		reuop.x	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜃))
21	19, 20	sbcie 3812	. . . . . . . . . . . . . . . . . . 19 ⊢ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 ↔ 𝜃)
22		pm2.27 42	. . . . . . . . . . . . . . . . . . 19 ⊢ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩))
23	21, 22	sylbir 237	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩))
24		eqcom 2828	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ = 𝑝 ↔ 𝑝 = ⟨𝑥, 𝑦⟩)
25	23, 24	syl6ibr 254	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ = 𝑝))
26	25	com12 32	. . . . . . . . . . . . . . . 16 ⊢ (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → (𝜃 → ⟨𝑥, 𝑦⟩ = 𝑝))
27		eqeq2 2833	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑎, 𝑏⟩ = 𝑝 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = 𝑝))
28	27	eqcoms 2829	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = 𝑝))
29	28	imbi2d 343	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ (𝜃 → ⟨𝑥, 𝑦⟩ = 𝑝)))
30	26, 29	syl5ibrcom 249	. . . . . . . . . . . . . . 15 ⊢ (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
31	30	a1d 25	. . . . . . . . . . . . . 14 ⊢ (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
32	18, 31	syl6 35	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝜓) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))))
33	32	expimpd 456	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))))
34	33	imp4c 426	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
35	34	impcom 410	. . . . . . . . . 10 ⊢ (((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
36	35	ralrimivva 3191	. . . . . . . . 9 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
37	11, 36	jca 514	. . . . . . . 8 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
38	37	ex 415	. . . . . . 7 ⊢ (((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
39	38	reximdvva 3277	. . . . . 6 ⊢ ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩ → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
40	39	com12 32	. . . . 5 ⊢ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
41	6, 40	sylbi 219	. . . 4 ⊢ (𝑝 ∈ (𝑋 × 𝑌) → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
42	41	rexlimiv 3280	. . 3 ⊢ (∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
43		opelxpi 5592	. . . . . . 7 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
44	43	adantr 483	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
45		simprl 769	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → 𝜒)
46		nfsbc1v 3792	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥[𝑐 / 𝑥]𝜃
47		nfv 1915	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩
48	46, 47	nfim 1897	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩)
49		nfsbc1v 3792	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦[𝑑 / 𝑦][𝑐 / 𝑥]𝜃
50		nfv 1915	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩
51	49, 50	nfim 1897	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
52		sbceq1a 3783	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → (𝜃 ↔ [𝑐 / 𝑥]𝜃))
53		opeq1 4803	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑐 → ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑦⟩)
54	53	eqeq1d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
55	52, 54	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → ((𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ ([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
56		sbceq1a 3783	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑑 → ([𝑐 / 𝑥]𝜃 ↔ [𝑑 / 𝑦][𝑐 / 𝑥]𝜃))
57		opeq2 4804	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑑 → ⟨𝑐, 𝑦⟩ = ⟨𝑐, 𝑑⟩)
58	57	eqeq1d 2823	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑑 → (⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
59	56, 58	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑑 → (([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
60	48, 51, 55, 59	rspc2 3631	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
61	60	ad2antlr 725	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) ∧ 𝜒) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
62	20	sbcop 5380	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 ↔ [⟨𝑐, 𝑑⟩ / 𝑝]𝜓)
63		pm2.27 42	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
64	62, 63	sylbir 237	. . . . . . . . . . . . . . . . 17 ⊢ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
65		eqcom 2828	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
66	64, 65	syl6ibr 254	. . . . . . . . . . . . . . . 16 ⊢ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
67	66	com12 32	. . . . . . . . . . . . . . 15 ⊢ (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
68	61, 67	syl6 35	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) ∧ 𝜒) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
69	68	expimpd 456	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
70	69	expcom 416	. . . . . . . . . . . 12 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))))
71	70	impd 413	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
72	71	impcom 410	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
73		dfsbcq 3774	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 ↔ [⟨𝑐, 𝑑⟩ / 𝑝]𝜓))
74		eqeq2 2833	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → (⟨𝑎, 𝑏⟩ = 𝑞 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
75	73, 74	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → (([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞) ↔ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
76	72, 75	syl5ibrcom 249	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → (𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
77	76	rexlimdvva 3294	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → (∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
78		elxp2 5579	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝑋 × 𝑌) ↔ ∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩)
79	78	biimpi 218	. . . . . . . 8 ⊢ (𝑞 ∈ (𝑋 × 𝑌) → ∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩)
80	77, 79	impel 508	. . . . . . 7 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ 𝑞 ∈ (𝑋 × 𝑌)) → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
81	80	ralrimiva 3182	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
82		nfv 1915	. . . . . . . 8 ⊢ Ⅎ𝑝𝜒
83		nfcv 2977	. . . . . . . . 9 ⊢ Ⅎ𝑝(𝑋 × 𝑌)
84		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑝⟨𝑎, 𝑏⟩ = 𝑞
85	1, 84	nfim 1897	. . . . . . . . 9 ⊢ Ⅎ𝑝([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)
86	83, 85	nfralw 3225	. . . . . . . 8 ⊢ Ⅎ𝑝∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)
87	82, 86	nfan 1900	. . . . . . 7 ⊢ Ⅎ𝑝(𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
88		eqeq1 2825	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝑝 = 𝑞 ↔ ⟨𝑎, 𝑏⟩ = 𝑞))
89	88	imbi2d 343	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
90	89	ralbidv 3197	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
91	7, 90	anbi12d 632	. . . . . . 7 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ↔ (𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))))
92	87, 91	rspce 3612	. . . . . 6 ⊢ ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌) ∧ (𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
93	44, 45, 81, 92	syl12anc 834	. . . . 5 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
94	93	ex 415	. . . 4 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞))))
95	94	rexlimivv 3292	. . 3 ⊢ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
96	42, 95	impbii 211	. 2 ⊢ (∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
97	5, 96	bitri 277	1 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139  ∃!wreu 3140  [wsbc 3772  ⟨cop 4573   × cxp 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5129  df-xp 5561

This theorem is referenced by:  ichnreuop  43683  ichreuopeq  43684  reuopreuprim  43737