Theorem reuop 6295

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 3759	. . 3 ⊢ Ⅎ𝑝[𝑞 / 𝑝]𝜓
2		nfsbc1v 3759	. . 3 ⊢ Ⅎ𝑝[𝑤 / 𝑝]𝜓
3		sbceq1a 3750	. . 3 ⊢ (𝑝 = 𝑤 → (𝜓 ↔ [𝑤 / 𝑝]𝜓))
4		dfsbcq 3741	. . 3 ⊢ (𝑤 = 𝑞 → ([𝑤 / 𝑝]𝜓 ↔ [𝑞 / 𝑝]𝜓))
5	1, 2, 3, 4	reu8nf 3824	. 2 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
6		elxp2 5675	. . . . 5 ⊢ (𝑝 ∈ (𝑋 × 𝑌) ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩)
7		reu3op.a	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜓 ↔ 𝜒))
8	7	biimpcd 252	. . . . . . . . . . . 12 ⊢ (𝜓 → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
9	8	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
10	9	adantr 486	. . . . . . . . . 10 ⊢ (((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → (𝑝 = ⟨𝑎, 𝑏⟩ → 𝜒))
11	10	imp 412	. . . . . . . . 9 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → 𝜒)
12		opelxpi 5688	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
13		dfsbcq 3741	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → ([𝑞 / 𝑝]𝜓 ↔ [⟨𝑥, 𝑦⟩ / 𝑝]𝜓))
14		eqeq2 2773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → (𝑝 = 𝑞 ↔ 𝑝 = ⟨𝑥, 𝑦⟩))
15	13, 14	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑥, 𝑦⟩ → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
16	15	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝑞 = ⟨𝑥, 𝑦⟩) → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
17	12, 16	rspcdv 3569	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
18	17	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ 𝜓) → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) → ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩)))
19		opex 5432	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
20		reuop.x	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜓 ↔ 𝜃))
21	19, 20	sbcie 3780	. . . . . . . . . . . . . . . . . . 19 ⊢ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 ↔ 𝜃)
22		pm2.27 43	. . . . . . . . . . . . . . . . . . 19 ⊢ ([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩))
23	21, 22	sylbir 238	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜃 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → 𝑝 = ⟨𝑥, 𝑦⟩))
24		eqcom 2768	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑥, 𝑦⟩ = 𝑝 ↔ 𝑝 = ⟨𝑥, 𝑦⟩)
25	23, 24	imbitrrdi 255	. . . . . . . . . . . . . . . . 17 ⊢ (𝜃 → (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ = 𝑝))
26	25	com12 33	. . . . . . . . . . . . . . . 16 ⊢ (([⟨𝑥, 𝑦⟩ / 𝑝]𝜓 → 𝑝 = ⟨𝑥, 𝑦⟩) → (𝜃 → ⟨𝑥, 𝑦⟩ = 𝑝))
27		eqeq2 2773	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑎, 𝑏⟩ = 𝑝 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑥, 𝑦⟩ = 𝑝))
28	27	eqcoms 2769	. . . . . . . . . . . . . . . . 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 459	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))))
34	33	imp4c 429	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
35	34	impcom 413	. . . . . . . . . 10 ⊢ (((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌)) → (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
36	35	ralrimivva 3206	. . . . . . . . 9 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
37	11, 36	jca 521	. . . . . . . 8 ⊢ ((((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) ∧ 𝑝 = ⟨𝑎, 𝑏⟩) → (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
38	37	ex 418	. . . . . . 7 ⊢ (((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌)) → (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
39	38	reximdvva 3211	. . . . . 6 ⊢ ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩ → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
40	39	com12 33	. . . . 5 ⊢ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
41	6, 40	sylbi 220	. . . 4 ⊢ (𝑝 ∈ (𝑋 × 𝑌) → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))))
42	41	rexlimiv 3157	. . 3 ⊢ (∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) → ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
43		opelxpi 5688	. . . . . . 7 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
44	43	adantr 486	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌))
45		simprl 783	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → 𝜒)
46		nfsbc1v 3759	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥[𝑐 / 𝑥]𝜃
47		nfv 1947	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑥⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩
48	46, 47	nfim 1929	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩)
49		nfsbc1v 3759	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦[𝑑 / 𝑦][𝑐 / 𝑥]𝜃
50		nfv 1947	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩
51	49, 50	nfim 1929	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑦([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
52		sbceq1a 3750	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → (𝜃 ↔ [𝑐 / 𝑥]𝜃))
53		opeq1 4833	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑐 → ⟨𝑥, 𝑦⟩ = ⟨𝑐, 𝑦⟩)
54	53	eqeq1d 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑐 → (⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩))
55	52, 54	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → ((𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ ([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
56		sbceq1a 3750	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑑 → ([𝑐 / 𝑥]𝜃 ↔ [𝑑 / 𝑦][𝑐 / 𝑥]𝜃))
57		opeq2 4834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑑 → ⟨𝑐, 𝑦⟩ = ⟨𝑐, 𝑑⟩)
58	57	eqeq1d 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑑 → (⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
59	56, 58	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑑 → (([𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑦⟩ = ⟨𝑎, 𝑏⟩) ↔ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
60	48, 51, 55, 59	rspc2 3585	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
61	60	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) ∧ 𝜒) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)))
62	20	sbcop 5459	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 ↔ [⟨𝑐, 𝑑⟩ / 𝑝]𝜓)
63		pm2.27 43	. . . . . . . . . . . . . . . . . 18 ⊢ ([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
64	62, 63	sylbir 238	. . . . . . . . . . . . . . . . 17 ⊢ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩))
65		eqcom 2768	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩ ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
66	64, 65	imbitrrdi 255	. . . . . . . . . . . . . . . 16 ⊢ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
67	66	com12 33	. . . . . . . . . . . . . . 15 ⊢ (([𝑑 / 𝑦][𝑐 / 𝑥]𝜃 → ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
68	61, 67	syl6 36	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) ∧ 𝜒) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
69	68	expimpd 459	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
70	69	expcom 419	. . . . . . . . . . . 12 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))))
71	70	impd 416	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌) → (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
72	71	impcom 413	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
73		dfsbcq 3741	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 ↔ [⟨𝑐, 𝑑⟩ / 𝑝]𝜓))
74		eqeq2 2773	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → (⟨𝑎, 𝑏⟩ = 𝑞 ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩))
75	73, 74	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑞 = ⟨𝑐, 𝑑⟩ → (([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞) ↔ ([⟨𝑐, 𝑑⟩ / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = ⟨𝑐, 𝑑⟩)))
76	72, 75	syl5ibrcom 250	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ (𝑐 ∈ 𝑋 ∧ 𝑑 ∈ 𝑌)) → (𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
77	76	rexlimdvva 3220	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → (∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩ → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
78		elxp2 5675	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝑋 × 𝑌) ↔ ∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩)
79	78	biimpi 219	. . . . . . . 8 ⊢ (𝑞 ∈ (𝑋 × 𝑌) → ∃𝑐 ∈ 𝑋 ∃𝑑 ∈ 𝑌 𝑞 = ⟨𝑐, 𝑑⟩)
80	77, 79	impel 515	. . . . . . 7 ⊢ ((((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) ∧ 𝑞 ∈ (𝑋 × 𝑌)) → ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
81	80	ralrimiva 3155	. . . . . 6 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
82		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑝𝜒
83		nfcv 2923	. . . . . . . . 9 ⊢ Ⅎ𝑝(𝑋 × 𝑌)
84		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑝⟨𝑎, 𝑏⟩ = 𝑞
85	1, 84	nfim 1929	. . . . . . . . 9 ⊢ Ⅎ𝑝([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)
86	83, 85	nfralw 3310	. . . . . . . 8 ⊢ Ⅎ𝑝∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)
87	82, 86	nfan 1932	. . . . . . 7 ⊢ Ⅎ𝑝(𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))
88		eqeq1 2765	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (𝑝 = 𝑞 ↔ ⟨𝑎, 𝑏⟩ = 𝑞))
89	88	imbi2d 343	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
90	89	ralbidv 3186	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → (∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞) ↔ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞)))
91	7, 90	anbi12d 644	. . . . . . 7 ⊢ (𝑝 = ⟨𝑎, 𝑏⟩ → ((𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ↔ (𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))))
92	87, 91	rspce 3566	. . . . . 6 ⊢ ((⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑌) ∧ (𝜒 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → ⟨𝑎, 𝑏⟩ = 𝑞))) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
93	44, 45, 81, 92	syl12anc 850	. . . . 5 ⊢ (((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) ∧ (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩))) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
94	93	ex 418	. . . 4 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌) → ((𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞))))
95	94	rexlimivv 3205	. . 3 ⊢ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)) → ∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)))
96	42, 95	impbii 212	. 2 ⊢ (∃𝑝 ∈ (𝑋 × 𝑌)(𝜓 ∧ ∀𝑞 ∈ (𝑋 × 𝑌)([𝑞 / 𝑝]𝜓 → 𝑝 = 𝑞)) ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))
97	5, 96	bitri 278	1 ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → ⟨𝑥, 𝑦⟩ = ⟨𝑎, 𝑏⟩)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087  ∃!wreu 3364  [wsbc 3739  ⟨cop 4590   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-xp 5657

This theorem is used by:  ichnreuop  48523  ichreuopeq  48524  reuopreuprim  48577