Theorem reuop 6185

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 3731	. . 3 ⊢ Ⅎ𝑝[𝑞 / 𝑝]𝜓
2		nfsbc1v 3731	. . 3 ⊢ Ⅎ𝑝[𝑤 / 𝑝]𝜓
3		sbceq1a 3722	. . 3 ⊢ (𝑝 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑝]𝜓))
4		dfsbcq 3713	. . 3 ⊢ (𝑤 = 𝑞 → ([𝑤 / 𝑝]𝜓 ↔ [𝑞 / 𝑝]𝜓))
5	1, 2, 3, 4	reu8nf 3806	. 2 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
6		elxp2 5604	. . . . 5 ⊢ (𝑝 ∈ (𝑋 × 𝑌) ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩)
7		reu3op.a	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜓 ↔ 𝜒))
8	7	biimpcd 248	. . . . . . . . . . . 12 ⊢ (𝜓 → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
9	8	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
10	9	adantr 480	. . . . . . . . . 10 ⊢ (((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
11	10	imp 406	. . . . . . . . 9 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → 𝜒)
12		opelxpi 5617	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
13		dfsbcq 3713	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → ([𝑞 / 𝑝]𝜓 ↔ [⟨𝑥, 𝑦⟩ / 𝑝]𝜓))
14		eqeq2 2750	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → (𝑝 = 𝑞 ↔ 𝑝 = ⟨𝑥, 𝑦⟩))
15	13, 14	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
16	15	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝑞 = ⟨𝑥, 𝑦⟩) → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
17	12, 16	rspcdv 3543	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
18	17	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝜓) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
19		opex 5373	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
20		reuop.x	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜃))
21	19, 20	sbcie 3754	. . . . . . . . . . . . . . . . . . 19 ⊢ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 ↔ 𝜃)
22		pm2.27 42	. . . . . . . . . . . . . . . . . . 19 ⊢ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩))
23	21, 22	sylbir 234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩))
24		eqcom 2745	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ = 𝑝 ↔ 𝑝 = ⟨𝑥, 𝑦⟩)
25	23, 24	syl6ibr 251	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ = 𝑝))
26	25	com12 32	. . . . . . . . . . . . . . . 16 ⊢ (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → (𝜃 → ⟨𝑥, 𝑦⟩ = 𝑝))
27		eqeq2 2750	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑎, 𝑏⟩ = 𝑝 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = 𝑝))
28	27	eqcoms 2746	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = 𝑝))
29	28	imbi2d 340	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ (𝜃 → ⟨𝑥, 𝑦⟩ = 𝑝)))
30	26, 29	syl5ibrcom 246	. . . . . . . . . . . . . . 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 3114	. . . . . . . . 9 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
37	11, 36	jca 511	. . . . . . . 8 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
38	37	ex 412	. . . . . . 7 ⊢ (((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
39	38	reximdvva 3205	. . . . . 6 ⊢ ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩ → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
40	39	com12 32	. . . . 5 ⊢ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
41	6, 40	sylbi 216	. . . 4 ⊢ (𝑝 ∈ (𝑋 × 𝑌) → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
42	41	rexlimiv 3208	. . 3 ⊢ (∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
43		opelxpi 5617	. . . . . . 7 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
44	43	adantr 480	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
45		simprl 767	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → 𝜒)
46		nfsbc1v 3731	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥[𝑐 / 𝑥]𝜃
47		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩
48	46, 47	nfim 1900	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩)
49		nfsbc1v 3731	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦[𝑑 / 𝑦][𝑐 / 𝑥]𝜃
50		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩
51	49, 50	nfim 1900	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
52		sbceq1a 3722	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → (𝜃 ↔ [𝑐 / 𝑥]𝜃))
53		opeq1 4801	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑐 → ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑦⟩)
54	53	eqeq1d 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
55	52, 54	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → ((𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ ([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
56		sbceq1a 3722	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑑 → ([𝑐 / 𝑥]𝜃 ↔ [𝑑 / 𝑦][𝑐 / 𝑥]𝜃))
57		opeq2 4802	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑑 → ⟨𝑐, 𝑦⟩ = ⟨𝑐, 𝑑⟩)
58	57	eqeq1d 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑑 → (⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
59	56, 58	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑑 → (([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
60	48, 51, 55, 59	rspc2 3560	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
61	60	ad2antlr 723	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) ∧ 𝜒) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
62	20	sbcop 5397	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 ↔ [⟨𝑐, 𝑑⟩ / 𝑝]𝜓)
63		pm2.27 42	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
64	62, 63	sylbir 234	. . . . . . . . . . . . . . . . 17 ⊢ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
65		eqcom 2745	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
66	64, 65	syl6ibr 251	. . . . . . . . . . . . . . . 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 3713	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 ↔ [⟨𝑐, 𝑑⟩ / 𝑝]𝜓))
74		eqeq2 2750	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → (⟨𝑎, 𝑏⟩ = 𝑞 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
75	73, 74	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → (([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞) ↔ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
76	72, 75	syl5ibrcom 246	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → (𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
77	76	rexlimdvva 3222	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → (∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
78		elxp2 5604	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝑋 × 𝑌) ↔ ∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩)
79	78	biimpi 215	. . . . . . . 8 ⊢ (𝑞 ∈ (𝑋 × 𝑌) → ∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩)
80	77, 79	impel 505	. . . . . . 7 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ 𝑞 ∈ (𝑋 × 𝑌)) → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
81	80	ralrimiva 3107	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
82		nfv 1918	. . . . . . . 8 ⊢ Ⅎ𝑝𝜒
83		nfcv 2906	. . . . . . . . 9 ⊢ Ⅎ𝑝(𝑋 × 𝑌)
84		nfv 1918	. . . . . . . . . 10 ⊢ Ⅎ𝑝⟨𝑎, 𝑏⟩ = 𝑞
85	1, 84	nfim 1900	. . . . . . . . 9 ⊢ Ⅎ𝑝([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)
86	83, 85	nfralw 3149	. . . . . . . 8 ⊢ Ⅎ𝑝∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)
87	82, 86	nfan 1903	. . . . . . 7 ⊢ Ⅎ𝑝(𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
88		eqeq1 2742	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝑝 = 𝑞 ↔ ⟨𝑎, 𝑏⟩ = 𝑞))
89	88	imbi2d 340	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
90	89	ralbidv 3120	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
91	7, 90	anbi12d 630	. . . . . . 7 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ↔ (𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))))
92	87, 91	rspce 3540	. . . . . 6 ⊢ ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌) ∧ (𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
93	44, 45, 81, 92	syl12anc 833	. . . . 5 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
94	93	ex 412	. . . 4 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞))))
95	94	rexlimivv 3220	. . 3 ⊢ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
96	42, 95	impbii 208	. 2 ⊢ (∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
97	5, 96	bitri 274	1 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064  ∃!wreu 3065  [wsbc 3711  ⟨cop 4564   × cxp 5578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133  df-xp 5586

This theorem is referenced by:  ichnreuop  44812  ichreuopeq  44813  reuopreuprim  44866