Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  opreu2reuALT Structured version   Visualization version   GIF version

Theorem opreu2reuALT 31405
Description: Correspondence between uniqueness of ordered pairs and double restricted existential uniqueness quantification. Alternate proof of one direction only, use opreu2reurex 6246 instead. (Contributed by Thierry Arnoux, 4-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
Ref Expression
opsbc2ie.a (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑𝜒))
Assertion
Ref Expression
opreu2reuALT ((∃!𝑎𝐴𝑏𝐵 𝜒 ∧ ∃!𝑏𝐵𝑎𝐴 𝜒) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
Distinct variable groups:   𝑎,𝑏,𝑝   𝜑,𝑎,𝑏   𝐴,𝑎,𝑏,𝑝   𝐵,𝑎,𝑏,𝑝   𝜒,𝑎,𝑏,𝑝
Allowed substitution hint:   𝜑(𝑝)

Proof of Theorem opreu2reuALT
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2reu4 4484 . 2 ((∃!𝑎𝐴𝑏𝐵 𝜒 ∧ ∃!𝑏𝐵𝑎𝐴 𝜒) ↔ (∃𝑎𝐴𝑏𝐵 𝜒 ∧ ∃𝑥𝐴𝑦𝐵𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))))
2 simpllr 774 . . . . . 6 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → 𝑥𝐴)
3 simplr 767 . . . . . 6 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → 𝑦𝐵)
4 opelxpi 5670 . . . . . 6 ((𝑥𝐴𝑦𝐵) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵))
52, 3, 4syl2anc 584 . . . . 5 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵))
6 nfre1 3268 . . . . . . . . 9 𝑎𝑎𝐴𝑏𝐵 𝜒
7 nfv 1917 . . . . . . . . 9 𝑎 𝑥𝐴
86, 7nfan 1902 . . . . . . . 8 𝑎(∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴)
9 nfv 1917 . . . . . . . 8 𝑎 𝑦𝐵
108, 9nfan 1902 . . . . . . 7 𝑎((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵)
11 nfra1 3267 . . . . . . 7 𝑎𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
1210, 11nfan 1902 . . . . . 6 𝑎(((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
13 nfcv 2907 . . . . . . 7 𝑎𝑦
14 nfsbc1v 3759 . . . . . . 7 𝑎[𝑥 / 𝑎]𝜒
1513, 14nfsbc 3764 . . . . . 6 𝑎[𝑦 / 𝑏][𝑥 / 𝑎]𝜒
16 nfcv 2907 . . . . . . . . . . . . 13 𝑏𝐴
17 nfre1 3268 . . . . . . . . . . . . 13 𝑏𝑏𝐵 𝜒
1816, 17nfrexw 3296 . . . . . . . . . . . 12 𝑏𝑎𝐴𝑏𝐵 𝜒
19 nfv 1917 . . . . . . . . . . . 12 𝑏 𝑥𝐴
2018, 19nfan 1902 . . . . . . . . . . 11 𝑏(∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴)
21 nfv 1917 . . . . . . . . . . 11 𝑏 𝑦𝐵
2220, 21nfan 1902 . . . . . . . . . 10 𝑏((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵)
23 nfcv 2907 . . . . . . . . . . 11 𝑏𝐴
24 nfra1 3267 . . . . . . . . . . 11 𝑏𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
2523, 24nfral 3347 . . . . . . . . . 10 𝑏𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
2622, 25nfan 1902 . . . . . . . . 9 𝑏(((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
27 nfv 1917 . . . . . . . . 9 𝑏 𝑎𝐴
2826, 27nfan 1902 . . . . . . . 8 𝑏((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴)
29 nfre1 3268 . . . . . . . 8 𝑏𝑏𝐵 𝜒
3028, 29nfan 1902 . . . . . . 7 𝑏(((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ ∃𝑏𝐵 𝜒)
31 nfsbc1v 3759 . . . . . . 7 𝑏[𝑦 / 𝑏][𝑥 / 𝑎]𝜒
32 rspa 3231 . . . . . . . . . . . 12 ((∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ∧ 𝑎𝐴) → ∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
3332ad5ant23 758 . . . . . . . . . . 11 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → ∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
34 simplr 767 . . . . . . . . . . 11 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝑏𝐵)
35 simpr 485 . . . . . . . . . . 11 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝜒)
36 rspa 3231 . . . . . . . . . . . 12 ((∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ∧ 𝑏𝐵) → (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
3736imp 407 . . . . . . . . . . 11 (((∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ∧ 𝑏𝐵) ∧ 𝜒) → (𝑎 = 𝑥𝑏 = 𝑦))
3833, 34, 35, 37syl21anc 836 . . . . . . . . . 10 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → (𝑎 = 𝑥𝑏 = 𝑦))
3938simprd 496 . . . . . . . . 9 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝑏 = 𝑦)
40 rspa 3231 . . . . . . . . . . . . 13 ((∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ∧ 𝑎𝐴) → ∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
4140ad5ant23 758 . . . . . . . . . . . 12 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → ∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
42 simplr 767 . . . . . . . . . . . 12 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝑏𝐵)
43 simpr 485 . . . . . . . . . . . 12 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝜒)
44 rspa 3231 . . . . . . . . . . . . 13 ((∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ∧ 𝑏𝐵) → (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
4544imp 407 . . . . . . . . . . . 12 (((∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ∧ 𝑏𝐵) ∧ 𝜒) → (𝑎 = 𝑥𝑏 = 𝑦))
4641, 42, 43, 45syl21anc 836 . . . . . . . . . . 11 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → (𝑎 = 𝑥𝑏 = 𝑦))
4746simpld 495 . . . . . . . . . 10 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝑎 = 𝑥)
48 simpr 485 . . . . . . . . . 10 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝜒)
49 sbceq1a 3750 . . . . . . . . . . 11 (𝑎 = 𝑥 → (𝜒[𝑥 / 𝑎]𝜒))
5049biimpa 477 . . . . . . . . . 10 ((𝑎 = 𝑥𝜒) → [𝑥 / 𝑎]𝜒)
5147, 48, 50syl2anc 584 . . . . . . . . 9 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → [𝑥 / 𝑎]𝜒)
52 sbceq1a 3750 . . . . . . . . . 10 (𝑏 = 𝑦 → ([𝑥 / 𝑎]𝜒[𝑦 / 𝑏][𝑥 / 𝑎]𝜒))
5352biimpa 477 . . . . . . . . 9 ((𝑏 = 𝑦[𝑥 / 𝑎]𝜒) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
5439, 51, 53syl2anc 584 . . . . . . . 8 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
5554adantllr 717 . . . . . . 7 ((((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ ∃𝑏𝐵 𝜒) ∧ 𝑏𝐵) ∧ 𝜒) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
56 simpr 485 . . . . . . 7 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ ∃𝑏𝐵 𝜒) → ∃𝑏𝐵 𝜒)
5730, 31, 55, 56r19.29af2 3250 . . . . . 6 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ ∃𝑏𝐵 𝜒) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
58 simplll 773 . . . . . 6 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → ∃𝑎𝐴𝑏𝐵 𝜒)
5912, 15, 57, 58r19.29af2 3250 . . . . 5 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
60 1st2nd2 7960 . . . . . . . . 9 (𝑝 ∈ (𝐴 × 𝐵) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
6160ad2antlr 725 . . . . . . . 8 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
62 nfre1 3268 . . . . . . . . . . . . . . . . . 18 𝑎𝑎𝐴𝑏𝐵 𝜒
63 nfv 1917 . . . . . . . . . . . . . . . . . 18 𝑎 𝑥𝐴
6462, 63nfan 1902 . . . . . . . . . . . . . . . . 17 𝑎(∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴)
65 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑎 𝑦𝐵
6664, 65nfan 1902 . . . . . . . . . . . . . . . 16 𝑎((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵)
67 nfra1 3267 . . . . . . . . . . . . . . . 16 𝑎𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
6866, 67nfan 1902 . . . . . . . . . . . . . . 15 𝑎(((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
69 nfv 1917 . . . . . . . . . . . . . . 15 𝑎 𝑝 ∈ (𝐴 × 𝐵)
7068, 69nfan 1902 . . . . . . . . . . . . . 14 𝑎((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵))
71 nfv 1917 . . . . . . . . . . . . . 14 𝑎𝜑
7270, 71nfan 1902 . . . . . . . . . . . . 13 𝑎(((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑)
73 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑏𝐴
74 nfre1 3268 . . . . . . . . . . . . . . . . . . 19 𝑏𝑏𝐵 𝜒
7573, 74nfrexw 3296 . . . . . . . . . . . . . . . . . 18 𝑏𝑎𝐴𝑏𝐵 𝜒
76 nfv 1917 . . . . . . . . . . . . . . . . . 18 𝑏 𝑥𝐴
7775, 76nfan 1902 . . . . . . . . . . . . . . . . 17 𝑏(∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴)
78 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑏 𝑦𝐵
7977, 78nfan 1902 . . . . . . . . . . . . . . . 16 𝑏((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵)
80 nfcv 2907 . . . . . . . . . . . . . . . . 17 𝑏𝐴
81 nfra1 3267 . . . . . . . . . . . . . . . . 17 𝑏𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
8280, 81nfral 3347 . . . . . . . . . . . . . . . 16 𝑏𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
8379, 82nfan 1902 . . . . . . . . . . . . . . 15 𝑏(((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
84 nfv 1917 . . . . . . . . . . . . . . 15 𝑏 𝑝 ∈ (𝐴 × 𝐵)
8583, 84nfan 1902 . . . . . . . . . . . . . 14 𝑏((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵))
86 nfv 1917 . . . . . . . . . . . . . 14 𝑏𝜑
8785, 86nfan 1902 . . . . . . . . . . . . 13 𝑏(((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑)
88 nfv 1917 . . . . . . . . . . . . 13 𝑎(𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))
89 nfv 1917 . . . . . . . . . . . . 13 𝑏(𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))
90 xp1st 7953 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝐴 × 𝐵) → (1st𝑝) ∈ 𝐴)
9190ad2antlr 725 . . . . . . . . . . . . 13 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (1st𝑝) ∈ 𝐴)
92 xp2nd 7954 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝐴 × 𝐵) → (2nd𝑝) ∈ 𝐵)
9392ad2antlr 725 . . . . . . . . . . . . 13 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (2nd𝑝) ∈ 𝐵)
94 eqcom 2743 . . . . . . . . . . . . . . . . 17 ((1st𝑝) = 𝑎𝑎 = (1st𝑝))
95 eqcom 2743 . . . . . . . . . . . . . . . . 17 ((2nd𝑝) = 𝑏𝑏 = (2nd𝑝))
96 eqopi 7957 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏)) → 𝑝 = ⟨𝑎, 𝑏⟩)
97 opsbc2ie.a . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑𝜒))
9896, 97syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏)) → (𝜑𝜒))
9998bicomd 222 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏)) → (𝜒𝜑))
10099ancoms 459 . . . . . . . . . . . . . . . . . 18 ((((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏) ∧ 𝑝 ∈ (𝐴 × 𝐵)) → (𝜒𝜑))
101100ex 413 . . . . . . . . . . . . . . . . 17 (((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏) → (𝑝 ∈ (𝐴 × 𝐵) → (𝜒𝜑)))
10294, 95, 101syl2anbr 599 . . . . . . . . . . . . . . . 16 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → (𝑝 ∈ (𝐴 × 𝐵) → (𝜒𝜑)))
103102impcom 408 . . . . . . . . . . . . . . 15 ((𝑝 ∈ (𝐴 × 𝐵) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → (𝜒𝜑))
104103ad4ant24 752 . . . . . . . . . . . . . 14 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → (𝜒𝜑))
105 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → 𝑎 = (1st𝑝))
106105eqeq1d 2738 . . . . . . . . . . . . . . . 16 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → (𝑎 = 𝑥 ↔ (1st𝑝) = 𝑥))
107 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → 𝑏 = (2nd𝑝))
108107eqeq1d 2738 . . . . . . . . . . . . . . . 16 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → (𝑏 = 𝑦 ↔ (2nd𝑝) = 𝑦))
109106, 108anbi12d 631 . . . . . . . . . . . . . . 15 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → ((𝑎 = 𝑥𝑏 = 𝑦) ↔ ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
110109adantl 482 . . . . . . . . . . . . . 14 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → ((𝑎 = 𝑥𝑏 = 𝑦) ↔ ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
111104, 110imbi12d 344 . . . . . . . . . . . . 13 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → ((𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ↔ (𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))))
112 simpllr 774 . . . . . . . . . . . . 13 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
11372, 87, 88, 89, 91, 93, 111, 112rspc2daf 31397 . . . . . . . . . . . 12 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
114113com12 32 . . . . . . . . . . 11 (𝜑 → ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
115114anabsi7 669 . . . . . . . . . 10 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))
116115simpld 495 . . . . . . . . 9 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (1st𝑝) = 𝑥)
117 nfre1 3268 . . . . . . . . . . . . . . . . . 18 𝑎𝑎𝐴𝑏𝐵 𝜒
118 nfv 1917 . . . . . . . . . . . . . . . . . 18 𝑎 𝑥𝐴
119117, 118nfan 1902 . . . . . . . . . . . . . . . . 17 𝑎(∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴)
120 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑎 𝑦𝐵
121119, 120nfan 1902 . . . . . . . . . . . . . . . 16 𝑎((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵)
122 nfra1 3267 . . . . . . . . . . . . . . . 16 𝑎𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
123121, 122nfan 1902 . . . . . . . . . . . . . . 15 𝑎(((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
124 nfv 1917 . . . . . . . . . . . . . . 15 𝑎 𝑝 ∈ (𝐴 × 𝐵)
125123, 124nfan 1902 . . . . . . . . . . . . . 14 𝑎((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵))
126 nfv 1917 . . . . . . . . . . . . . 14 𝑎𝜑
127125, 126nfan 1902 . . . . . . . . . . . . 13 𝑎(((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑)
128 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑏𝐴
129 nfre1 3268 . . . . . . . . . . . . . . . . . . 19 𝑏𝑏𝐵 𝜒
130128, 129nfrexw 3296 . . . . . . . . . . . . . . . . . 18 𝑏𝑎𝐴𝑏𝐵 𝜒
131 nfv 1917 . . . . . . . . . . . . . . . . . 18 𝑏 𝑥𝐴
132130, 131nfan 1902 . . . . . . . . . . . . . . . . 17 𝑏(∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴)
133 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑏 𝑦𝐵
134132, 133nfan 1902 . . . . . . . . . . . . . . . 16 𝑏((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵)
135 nfcv 2907 . . . . . . . . . . . . . . . . 17 𝑏𝐴
136 nfra1 3267 . . . . . . . . . . . . . . . . 17 𝑏𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
137135, 136nfral 3347 . . . . . . . . . . . . . . . 16 𝑏𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
138134, 137nfan 1902 . . . . . . . . . . . . . . 15 𝑏(((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
139 nfv 1917 . . . . . . . . . . . . . . 15 𝑏 𝑝 ∈ (𝐴 × 𝐵)
140138, 139nfan 1902 . . . . . . . . . . . . . 14 𝑏((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵))
141 nfv 1917 . . . . . . . . . . . . . 14 𝑏𝜑
142140, 141nfan 1902 . . . . . . . . . . . . 13 𝑏(((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑)
143 nfv 1917 . . . . . . . . . . . . 13 𝑎(𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))
144 nfv 1917 . . . . . . . . . . . . 13 𝑏(𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))
145 xp1st 7953 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝐴 × 𝐵) → (1st𝑝) ∈ 𝐴)
146145ad2antlr 725 . . . . . . . . . . . . 13 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (1st𝑝) ∈ 𝐴)
147 xp2nd 7954 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝐴 × 𝐵) → (2nd𝑝) ∈ 𝐵)
148147ad2antlr 725 . . . . . . . . . . . . 13 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (2nd𝑝) ∈ 𝐵)
149 eqcom 2743 . . . . . . . . . . . . . . . . 17 ((1st𝑝) = 𝑎𝑎 = (1st𝑝))
150 eqcom 2743 . . . . . . . . . . . . . . . . 17 ((2nd𝑝) = 𝑏𝑏 = (2nd𝑝))
151 eqopi 7957 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏)) → 𝑝 = ⟨𝑎, 𝑏⟩)
152151, 97syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏)) → (𝜑𝜒))
153152bicomd 222 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏)) → (𝜒𝜑))
154153ancoms 459 . . . . . . . . . . . . . . . . . 18 ((((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏) ∧ 𝑝 ∈ (𝐴 × 𝐵)) → (𝜒𝜑))
155154ex 413 . . . . . . . . . . . . . . . . 17 (((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏) → (𝑝 ∈ (𝐴 × 𝐵) → (𝜒𝜑)))
156149, 150, 155syl2anbr 599 . . . . . . . . . . . . . . . 16 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → (𝑝 ∈ (𝐴 × 𝐵) → (𝜒𝜑)))
157156impcom 408 . . . . . . . . . . . . . . 15 ((𝑝 ∈ (𝐴 × 𝐵) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → (𝜒𝜑))
158157ad4ant24 752 . . . . . . . . . . . . . 14 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → (𝜒𝜑))
159 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → 𝑎 = (1st𝑝))
160159eqeq1d 2738 . . . . . . . . . . . . . . . 16 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → (𝑎 = 𝑥 ↔ (1st𝑝) = 𝑥))
161 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → 𝑏 = (2nd𝑝))
162161eqeq1d 2738 . . . . . . . . . . . . . . . 16 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → (𝑏 = 𝑦 ↔ (2nd𝑝) = 𝑦))
163160, 162anbi12d 631 . . . . . . . . . . . . . . 15 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → ((𝑎 = 𝑥𝑏 = 𝑦) ↔ ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
164163adantl 482 . . . . . . . . . . . . . 14 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → ((𝑎 = 𝑥𝑏 = 𝑦) ↔ ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
165158, 164imbi12d 344 . . . . . . . . . . . . 13 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → ((𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ↔ (𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))))
166 simpllr 774 . . . . . . . . . . . . 13 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
167127, 142, 143, 144, 146, 148, 165, 166rspc2daf 31397 . . . . . . . . . . . 12 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
168167com12 32 . . . . . . . . . . 11 (𝜑 → ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
169168anabsi7 669 . . . . . . . . . 10 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))
170169simprd 496 . . . . . . . . 9 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (2nd𝑝) = 𝑦)
171116, 170opeq12d 4838 . . . . . . . 8 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ⟨(1st𝑝), (2nd𝑝)⟩ = ⟨𝑥, 𝑦⟩)
17261, 171eqtrd 2776 . . . . . . 7 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → 𝑝 = ⟨𝑥, 𝑦⟩)
173172ex 413 . . . . . 6 (((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) → (𝜑𝑝 = ⟨𝑥, 𝑦⟩))
174173ralrimiva 3143 . . . . 5 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → ∀𝑝 ∈ (𝐴 × 𝐵)(𝜑𝑝 = ⟨𝑥, 𝑦⟩))
1755, 59, 1743jca 1128 . . . 4 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒 ∧ ∀𝑝 ∈ (𝐴 × 𝐵)(𝜑𝑝 = ⟨𝑥, 𝑦⟩)))
17697opsbc2ie 31404 . . . . 5 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜑[𝑦 / 𝑏][𝑥 / 𝑎]𝜒))
177176eqreu 3687 . . . 4 ((⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒 ∧ ∀𝑝 ∈ (𝐴 × 𝐵)(𝜑𝑝 = ⟨𝑥, 𝑦⟩)) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
178175, 177syl 17 . . 3 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
179178r19.29ffa 31402 . 2 ((∃𝑎𝐴𝑏𝐵 𝜒 ∧ ∃𝑥𝐴𝑦𝐵𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
1801, 179sylbi 216 1 ((∃!𝑎𝐴𝑏𝐵 𝜒 ∧ ∃!𝑏𝐵𝑎𝐴 𝜒) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073  ∃!wreu 3351  [wsbc 3739  cop 4592   × cxp 5631  cfv 6496  1st c1st 7919  2nd c2nd 7920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2370  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-iota 6448  df-fun 6498  df-fv 6504  df-1st 7921  df-2nd 7922
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator