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

Theorem opreu2reuALT 30346
 Description: Correspondence between uniqueness of ordered pairs and double restricted existential uniqueness quantification. Alternate proof of one direction only, use opreu2reurex 6123 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 4419 . 2 ((∃!𝑎𝐴𝑏𝐵 𝜒 ∧ ∃!𝑏𝐵𝑎𝐴 𝜒) ↔ (∃𝑎𝐴𝑏𝐵 𝜒 ∧ ∃𝑥𝐴𝑦𝐵𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))))
2 simpllr 775 . . . . . 6 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → 𝑥𝐴)
3 simplr 768 . . . . . 6 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → 𝑦𝐵)
4 opelxpi 5561 . . . . . 6 ((𝑥𝐴𝑦𝐵) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵))
52, 3, 4syl2anc 587 . . . . 5 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵))
6 nfre1 3230 . . . . . . . . 9 𝑎𝑎𝐴𝑏𝐵 𝜒
7 nfv 1915 . . . . . . . . 9 𝑎 𝑥𝐴
86, 7nfan 1900 . . . . . . . 8 𝑎(∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴)
9 nfv 1915 . . . . . . . 8 𝑎 𝑦𝐵
108, 9nfan 1900 . . . . . . 7 𝑎((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵)
11 nfra1 3147 . . . . . . 7 𝑎𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
1210, 11nfan 1900 . . . . . 6 𝑎(((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
13 nfcv 2919 . . . . . . 7 𝑎𝑦
14 nfsbc1v 3716 . . . . . . 7 𝑎[𝑥 / 𝑎]𝜒
1513, 14nfsbc 3721 . . . . . 6 𝑎[𝑦 / 𝑏][𝑥 / 𝑎]𝜒
16 nfcv 2919 . . . . . . . . . . . . 13 𝑏𝐴
17 nfre1 3230 . . . . . . . . . . . . 13 𝑏𝑏𝐵 𝜒
1816, 17nfrex 3233 . . . . . . . . . . . 12 𝑏𝑎𝐴𝑏𝐵 𝜒
19 nfv 1915 . . . . . . . . . . . 12 𝑏 𝑥𝐴
2018, 19nfan 1900 . . . . . . . . . . 11 𝑏(∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴)
21 nfv 1915 . . . . . . . . . . 11 𝑏 𝑦𝐵
2220, 21nfan 1900 . . . . . . . . . 10 𝑏((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵)
23 nfcv 2919 . . . . . . . . . . 11 𝑏𝐴
24 nfra1 3147 . . . . . . . . . . 11 𝑏𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
2523, 24nfral 3154 . . . . . . . . . 10 𝑏𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
2622, 25nfan 1900 . . . . . . . . 9 𝑏(((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
27 nfv 1915 . . . . . . . . 9 𝑏 𝑎𝐴
2826, 27nfan 1900 . . . . . . . 8 𝑏((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴)
29 nfre1 3230 . . . . . . . 8 𝑏𝑏𝐵 𝜒
3028, 29nfan 1900 . . . . . . 7 𝑏(((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ ∃𝑏𝐵 𝜒)
31 nfsbc1v 3716 . . . . . . 7 𝑏[𝑦 / 𝑏][𝑥 / 𝑎]𝜒
32 rspa 3135 . . . . . . . . . . . 12 ((∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ∧ 𝑎𝐴) → ∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
3332ad5ant23 759 . . . . . . . . . . 11 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → ∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
34 simplr 768 . . . . . . . . . . 11 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝑏𝐵)
35 simpr 488 . . . . . . . . . . 11 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝜒)
36 rspa 3135 . . . . . . . . . . . 12 ((∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ∧ 𝑏𝐵) → (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
3736imp 410 . . . . . . . . . . 11 (((∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ∧ 𝑏𝐵) ∧ 𝜒) → (𝑎 = 𝑥𝑏 = 𝑦))
3833, 34, 35, 37syl21anc 836 . . . . . . . . . 10 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → (𝑎 = 𝑥𝑏 = 𝑦))
3938simprd 499 . . . . . . . . 9 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝑏 = 𝑦)
40 rspa 3135 . . . . . . . . . . . . 13 ((∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ∧ 𝑎𝐴) → ∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
4140ad5ant23 759 . . . . . . . . . . . 12 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → ∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
42 simplr 768 . . . . . . . . . . . 12 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝑏𝐵)
43 simpr 488 . . . . . . . . . . . 12 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝜒)
44 rspa 3135 . . . . . . . . . . . . 13 ((∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ∧ 𝑏𝐵) → (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
4544imp 410 . . . . . . . . . . . 12 (((∀𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ∧ 𝑏𝐵) ∧ 𝜒) → (𝑎 = 𝑥𝑏 = 𝑦))
4641, 42, 43, 45syl21anc 836 . . . . . . . . . . 11 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → (𝑎 = 𝑥𝑏 = 𝑦))
4746simpld 498 . . . . . . . . . 10 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝑎 = 𝑥)
48 simpr 488 . . . . . . . . . 10 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → 𝜒)
49 sbceq1a 3707 . . . . . . . . . . 11 (𝑎 = 𝑥 → (𝜒[𝑥 / 𝑎]𝜒))
5049biimpa 480 . . . . . . . . . 10 ((𝑎 = 𝑥𝜒) → [𝑥 / 𝑎]𝜒)
5147, 48, 50syl2anc 587 . . . . . . . . 9 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → [𝑥 / 𝑎]𝜒)
52 sbceq1a 3707 . . . . . . . . . 10 (𝑏 = 𝑦 → ([𝑥 / 𝑎]𝜒[𝑦 / 𝑏][𝑥 / 𝑎]𝜒))
5352biimpa 480 . . . . . . . . 9 ((𝑏 = 𝑦[𝑥 / 𝑎]𝜒) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
5439, 51, 53syl2anc 587 . . . . . . . 8 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ 𝑏𝐵) ∧ 𝜒) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
5554adantllr 718 . . . . . . 7 ((((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ ∃𝑏𝐵 𝜒) ∧ 𝑏𝐵) ∧ 𝜒) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
56 simpr 488 . . . . . . 7 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ ∃𝑏𝐵 𝜒) → ∃𝑏𝐵 𝜒)
5730, 31, 55, 56r19.29af2 3253 . . . . . 6 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑎𝐴) ∧ ∃𝑏𝐵 𝜒) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
58 simplll 774 . . . . . 6 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → ∃𝑎𝐴𝑏𝐵 𝜒)
5912, 15, 57, 58r19.29af2 3253 . . . . 5 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → [𝑦 / 𝑏][𝑥 / 𝑎]𝜒)
60 1st2nd2 7732 . . . . . . . . 9 (𝑝 ∈ (𝐴 × 𝐵) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
6160ad2antlr 726 . . . . . . . 8 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → 𝑝 = ⟨(1st𝑝), (2nd𝑝)⟩)
62 nfre1 3230 . . . . . . . . . . . . . . . . . 18 𝑎𝑎𝐴𝑏𝐵 𝜒
63 nfv 1915 . . . . . . . . . . . . . . . . . 18 𝑎 𝑥𝐴
6462, 63nfan 1900 . . . . . . . . . . . . . . . . 17 𝑎(∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴)
65 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑎 𝑦𝐵
6664, 65nfan 1900 . . . . . . . . . . . . . . . 16 𝑎((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵)
67 nfra1 3147 . . . . . . . . . . . . . . . 16 𝑎𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
6866, 67nfan 1900 . . . . . . . . . . . . . . 15 𝑎(((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
69 nfv 1915 . . . . . . . . . . . . . . 15 𝑎 𝑝 ∈ (𝐴 × 𝐵)
7068, 69nfan 1900 . . . . . . . . . . . . . 14 𝑎((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵))
71 nfv 1915 . . . . . . . . . . . . . 14 𝑎𝜑
7270, 71nfan 1900 . . . . . . . . . . . . 13 𝑎(((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑)
73 nfcv 2919 . . . . . . . . . . . . . . . . . . 19 𝑏𝐴
74 nfre1 3230 . . . . . . . . . . . . . . . . . . 19 𝑏𝑏𝐵 𝜒
7573, 74nfrex 3233 . . . . . . . . . . . . . . . . . 18 𝑏𝑎𝐴𝑏𝐵 𝜒
76 nfv 1915 . . . . . . . . . . . . . . . . . 18 𝑏 𝑥𝐴
7775, 76nfan 1900 . . . . . . . . . . . . . . . . 17 𝑏(∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴)
78 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑏 𝑦𝐵
7977, 78nfan 1900 . . . . . . . . . . . . . . . 16 𝑏((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵)
80 nfcv 2919 . . . . . . . . . . . . . . . . 17 𝑏𝐴
81 nfra1 3147 . . . . . . . . . . . . . . . . 17 𝑏𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
8280, 81nfral 3154 . . . . . . . . . . . . . . . 16 𝑏𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
8379, 82nfan 1900 . . . . . . . . . . . . . . 15 𝑏(((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
84 nfv 1915 . . . . . . . . . . . . . . 15 𝑏 𝑝 ∈ (𝐴 × 𝐵)
8583, 84nfan 1900 . . . . . . . . . . . . . 14 𝑏((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵))
86 nfv 1915 . . . . . . . . . . . . . 14 𝑏𝜑
8785, 86nfan 1900 . . . . . . . . . . . . 13 𝑏(((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑)
88 nfv 1915 . . . . . . . . . . . . 13 𝑎(𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))
89 nfv 1915 . . . . . . . . . . . . 13 𝑏(𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))
90 xp1st 7725 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝐴 × 𝐵) → (1st𝑝) ∈ 𝐴)
9190ad2antlr 726 . . . . . . . . . . . . 13 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (1st𝑝) ∈ 𝐴)
92 xp2nd 7726 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝐴 × 𝐵) → (2nd𝑝) ∈ 𝐵)
9392ad2antlr 726 . . . . . . . . . . . . 13 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (2nd𝑝) ∈ 𝐵)
94 eqcom 2765 . . . . . . . . . . . . . . . . 17 ((1st𝑝) = 𝑎𝑎 = (1st𝑝))
95 eqcom 2765 . . . . . . . . . . . . . . . . 17 ((2nd𝑝) = 𝑏𝑏 = (2nd𝑝))
96 eqopi 7729 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏)) → 𝑝 = ⟨𝑎, 𝑏⟩)
97 opsbc2ie.a . . . . . . . . . . . . . . . . . . . . 21 (𝑝 = ⟨𝑎, 𝑏⟩ → (𝜑𝜒))
9896, 97syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏)) → (𝜑𝜒))
9998bicomd 226 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏)) → (𝜒𝜑))
10099ancoms 462 . . . . . . . . . . . . . . . . . 18 ((((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏) ∧ 𝑝 ∈ (𝐴 × 𝐵)) → (𝜒𝜑))
101100ex 416 . . . . . . . . . . . . . . . . 17 (((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏) → (𝑝 ∈ (𝐴 × 𝐵) → (𝜒𝜑)))
10294, 95, 101syl2anbr 601 . . . . . . . . . . . . . . . 16 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → (𝑝 ∈ (𝐴 × 𝐵) → (𝜒𝜑)))
103102impcom 411 . . . . . . . . . . . . . . 15 ((𝑝 ∈ (𝐴 × 𝐵) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → (𝜒𝜑))
104103ad4ant24 753 . . . . . . . . . . . . . 14 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → (𝜒𝜑))
105 simpl 486 . . . . . . . . . . . . . . . . 17 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → 𝑎 = (1st𝑝))
106105eqeq1d 2760 . . . . . . . . . . . . . . . 16 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → (𝑎 = 𝑥 ↔ (1st𝑝) = 𝑥))
107 simpr 488 . . . . . . . . . . . . . . . . 17 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → 𝑏 = (2nd𝑝))
108107eqeq1d 2760 . . . . . . . . . . . . . . . 16 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → (𝑏 = 𝑦 ↔ (2nd𝑝) = 𝑦))
109106, 108anbi12d 633 . . . . . . . . . . . . . . 15 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → ((𝑎 = 𝑥𝑏 = 𝑦) ↔ ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
110109adantl 485 . . . . . . . . . . . . . 14 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → ((𝑎 = 𝑥𝑏 = 𝑦) ↔ ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
111104, 110imbi12d 348 . . . . . . . . . . . . 13 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → ((𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ↔ (𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))))
112 simpllr 775 . . . . . . . . . . . . 13 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
11372, 87, 88, 89, 91, 93, 111, 112rspc2daf 30337 . . . . . . . . . . . 12 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
114113com12 32 . . . . . . . . . . 11 (𝜑 → ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
115114anabsi7 670 . . . . . . . . . 10 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))
116115simpld 498 . . . . . . . . 9 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (1st𝑝) = 𝑥)
117 nfre1 3230 . . . . . . . . . . . . . . . . . 18 𝑎𝑎𝐴𝑏𝐵 𝜒
118 nfv 1915 . . . . . . . . . . . . . . . . . 18 𝑎 𝑥𝐴
119117, 118nfan 1900 . . . . . . . . . . . . . . . . 17 𝑎(∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴)
120 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑎 𝑦𝐵
121119, 120nfan 1900 . . . . . . . . . . . . . . . 16 𝑎((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵)
122 nfra1 3147 . . . . . . . . . . . . . . . 16 𝑎𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
123121, 122nfan 1900 . . . . . . . . . . . . . . 15 𝑎(((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
124 nfv 1915 . . . . . . . . . . . . . . 15 𝑎 𝑝 ∈ (𝐴 × 𝐵)
125123, 124nfan 1900 . . . . . . . . . . . . . 14 𝑎((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵))
126 nfv 1915 . . . . . . . . . . . . . 14 𝑎𝜑
127125, 126nfan 1900 . . . . . . . . . . . . 13 𝑎(((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑)
128 nfcv 2919 . . . . . . . . . . . . . . . . . . 19 𝑏𝐴
129 nfre1 3230 . . . . . . . . . . . . . . . . . . 19 𝑏𝑏𝐵 𝜒
130128, 129nfrex 3233 . . . . . . . . . . . . . . . . . 18 𝑏𝑎𝐴𝑏𝐵 𝜒
131 nfv 1915 . . . . . . . . . . . . . . . . . 18 𝑏 𝑥𝐴
132130, 131nfan 1900 . . . . . . . . . . . . . . . . 17 𝑏(∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴)
133 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑏 𝑦𝐵
134132, 133nfan 1900 . . . . . . . . . . . . . . . 16 𝑏((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵)
135 nfcv 2919 . . . . . . . . . . . . . . . . 17 𝑏𝐴
136 nfra1 3147 . . . . . . . . . . . . . . . . 17 𝑏𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
137135, 136nfral 3154 . . . . . . . . . . . . . . . 16 𝑏𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))
138134, 137nfan 1900 . . . . . . . . . . . . . . 15 𝑏(((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
139 nfv 1915 . . . . . . . . . . . . . . 15 𝑏 𝑝 ∈ (𝐴 × 𝐵)
140138, 139nfan 1900 . . . . . . . . . . . . . 14 𝑏((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵))
141 nfv 1915 . . . . . . . . . . . . . 14 𝑏𝜑
142140, 141nfan 1900 . . . . . . . . . . . . 13 𝑏(((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑)
143 nfv 1915 . . . . . . . . . . . . 13 𝑎(𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))
144 nfv 1915 . . . . . . . . . . . . 13 𝑏(𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))
145 xp1st 7725 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝐴 × 𝐵) → (1st𝑝) ∈ 𝐴)
146145ad2antlr 726 . . . . . . . . . . . . 13 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (1st𝑝) ∈ 𝐴)
147 xp2nd 7726 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝐴 × 𝐵) → (2nd𝑝) ∈ 𝐵)
148147ad2antlr 726 . . . . . . . . . . . . 13 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (2nd𝑝) ∈ 𝐵)
149 eqcom 2765 . . . . . . . . . . . . . . . . 17 ((1st𝑝) = 𝑎𝑎 = (1st𝑝))
150 eqcom 2765 . . . . . . . . . . . . . . . . 17 ((2nd𝑝) = 𝑏𝑏 = (2nd𝑝))
151 eqopi 7729 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏)) → 𝑝 = ⟨𝑎, 𝑏⟩)
152151, 97syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏)) → (𝜑𝜒))
153152bicomd 226 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ∈ (𝐴 × 𝐵) ∧ ((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏)) → (𝜒𝜑))
154153ancoms 462 . . . . . . . . . . . . . . . . . 18 ((((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏) ∧ 𝑝 ∈ (𝐴 × 𝐵)) → (𝜒𝜑))
155154ex 416 . . . . . . . . . . . . . . . . 17 (((1st𝑝) = 𝑎 ∧ (2nd𝑝) = 𝑏) → (𝑝 ∈ (𝐴 × 𝐵) → (𝜒𝜑)))
156149, 150, 155syl2anbr 601 . . . . . . . . . . . . . . . 16 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → (𝑝 ∈ (𝐴 × 𝐵) → (𝜒𝜑)))
157156impcom 411 . . . . . . . . . . . . . . 15 ((𝑝 ∈ (𝐴 × 𝐵) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → (𝜒𝜑))
158157ad4ant24 753 . . . . . . . . . . . . . 14 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → (𝜒𝜑))
159 simpl 486 . . . . . . . . . . . . . . . . 17 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → 𝑎 = (1st𝑝))
160159eqeq1d 2760 . . . . . . . . . . . . . . . 16 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → (𝑎 = 𝑥 ↔ (1st𝑝) = 𝑥))
161 simpr 488 . . . . . . . . . . . . . . . . 17 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → 𝑏 = (2nd𝑝))
162161eqeq1d 2760 . . . . . . . . . . . . . . . 16 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → (𝑏 = 𝑦 ↔ (2nd𝑝) = 𝑦))
163160, 162anbi12d 633 . . . . . . . . . . . . . . 15 ((𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝)) → ((𝑎 = 𝑥𝑏 = 𝑦) ↔ ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
164163adantl 485 . . . . . . . . . . . . . 14 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → ((𝑎 = 𝑥𝑏 = 𝑦) ↔ ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
165158, 164imbi12d 348 . . . . . . . . . . . . 13 (((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) ∧ (𝑎 = (1st𝑝) ∧ 𝑏 = (2nd𝑝))) → ((𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)) ↔ (𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))))
166 simpllr 775 . . . . . . . . . . . . 13 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦)))
167127, 142, 143, 144, 146, 148, 165, 166rspc2daf 30337 . . . . . . . . . . . 12 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (𝜑 → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
168167com12 32 . . . . . . . . . . 11 (𝜑 → ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦)))
169168anabsi7 670 . . . . . . . . . 10 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ((1st𝑝) = 𝑥 ∧ (2nd𝑝) = 𝑦))
170169simprd 499 . . . . . . . . 9 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → (2nd𝑝) = 𝑦)
171116, 170opeq12d 4771 . . . . . . . 8 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → ⟨(1st𝑝), (2nd𝑝)⟩ = ⟨𝑥, 𝑦⟩)
17261, 171eqtrd 2793 . . . . . . 7 ((((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ 𝜑) → 𝑝 = ⟨𝑥, 𝑦⟩)
173172ex 416 . . . . . 6 (((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) ∧ 𝑝 ∈ (𝐴 × 𝐵)) → (𝜑𝑝 = ⟨𝑥, 𝑦⟩))
174173ralrimiva 3113 . . . . 5 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → ∀𝑝 ∈ (𝐴 × 𝐵)(𝜑𝑝 = ⟨𝑥, 𝑦⟩))
1755, 59, 1743jca 1125 . . . 4 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → (⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒 ∧ ∀𝑝 ∈ (𝐴 × 𝐵)(𝜑𝑝 = ⟨𝑥, 𝑦⟩)))
17697opsbc2ie 30345 . . . . 5 (𝑝 = ⟨𝑥, 𝑦⟩ → (𝜑[𝑦 / 𝑏][𝑥 / 𝑎]𝜒))
177176eqreu 3643 . . . 4 ((⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ [𝑦 / 𝑏][𝑥 / 𝑎]𝜒 ∧ ∀𝑝 ∈ (𝐴 × 𝐵)(𝜑𝑝 = ⟨𝑥, 𝑦⟩)) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
178175, 177syl 17 . . 3 ((((∃𝑎𝐴𝑏𝐵 𝜒𝑥𝐴) ∧ 𝑦𝐵) ∧ ∀𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
179178r19.29ffa 30343 . 2 ((∃𝑎𝐴𝑏𝐵 𝜒 ∧ ∃𝑥𝐴𝑦𝐵𝑎𝐴𝑏𝐵 (𝜒 → (𝑎 = 𝑥𝑏 = 𝑦))) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
1801, 179sylbi 220 1 ((∃!𝑎𝐴𝑏𝐵 𝜒 ∧ ∃!𝑏𝐵𝑎𝐴 𝜒) → ∃!𝑝 ∈ (𝐴 × 𝐵)𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071  ∃!wreu 3072  [wsbc 3696  ⟨cop 4528   × cxp 5522  ‘cfv 6335  1st c1st 7691  2nd c2nd 7692 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-13 2379  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-iota 6294  df-fun 6337  df-fv 6343  df-1st 7693  df-2nd 7694 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator