Step | Hyp | Ref
| Expression |
1 | | elxp 5542 |
. . . . 5
⊢ (𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑖∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))) |
2 | 1 | rexbii 3160 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))) |
3 | | rexcom4 3162 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 ∃𝑖∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))) |
4 | | rexcom4 3162 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))) |
5 | 4 | exbii 1854 |
. . . 4
⊢
(∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))) |
6 | 2, 3, 5 | 3bitri 300 |
. . 3
⊢
(∃𝑥 ∈
𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))) |
7 | | eliun 4882 |
. . 3
⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥}))) |
8 | | eldif 3851 |
. . . . . . 7
⊢
(〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ (〈𝑖, 𝑗〉 ∈ (𝐴 × 𝐵) ∧ ¬ 〈𝑖, 𝑗〉 ∈ I )) |
9 | | opelxp 5555 |
. . . . . . . 8
⊢
(〈𝑖, 𝑗〉 ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) |
10 | | df-br 5028 |
. . . . . . . . . 10
⊢ (𝑖 I 𝑗 ↔ 〈𝑖, 𝑗〉 ∈ I ) |
11 | | vex 3401 |
. . . . . . . . . . 11
⊢ 𝑗 ∈ V |
12 | 11 | ideq 5689 |
. . . . . . . . . 10
⊢ (𝑖 I 𝑗 ↔ 𝑖 = 𝑗) |
13 | 10, 12 | bitr3i 280 |
. . . . . . . . 9
⊢
(〈𝑖, 𝑗〉 ∈ I ↔ 𝑖 = 𝑗) |
14 | 13 | necon3bbii 2981 |
. . . . . . . 8
⊢ (¬
〈𝑖, 𝑗〉 ∈ I ↔ 𝑖 ≠ 𝑗) |
15 | 9, 14 | anbi12i 630 |
. . . . . . 7
⊢
((〈𝑖, 𝑗〉 ∈ (𝐴 × 𝐵) ∧ ¬ 〈𝑖, 𝑗〉 ∈ I ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)) |
16 | 8, 15 | bitri 278 |
. . . . . 6
⊢
(〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)) |
17 | 16 | anbi2i 626 |
. . . . 5
⊢ ((𝑝 = 〈𝑖, 𝑗〉 ∧ 〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I )) ↔ (𝑝 = 〈𝑖, 𝑗〉 ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))) |
18 | 17 | 2exbii 1855 |
. . . 4
⊢
(∃𝑖∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ 〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I )) ↔ ∃𝑖∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))) |
19 | | eldifi 4015 |
. . . . . . . . 9
⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → 𝑝 ∈ (𝐴 × 𝐵)) |
20 | | elxpi 5541 |
. . . . . . . . 9
⊢ (𝑝 ∈ (𝐴 × 𝐵) → ∃𝑖∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))) |
21 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → 𝑝 = 〈𝑖, 𝑗〉) |
22 | 21 | 2eximi 1842 |
. . . . . . . . 9
⊢
(∃𝑖∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → ∃𝑖∃𝑗 𝑝 = 〈𝑖, 𝑗〉) |
23 | 19, 20, 22 | 3syl 18 |
. . . . . . . 8
⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗 𝑝 = 〈𝑖, 𝑗〉) |
24 | 23 | ancli 552 |
. . . . . . 7
⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ ∃𝑖∃𝑗 𝑝 = 〈𝑖, 𝑗〉)) |
25 | | 19.42vv 1964 |
. . . . . . 7
⊢
(∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = 〈𝑖, 𝑗〉) ↔ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ ∃𝑖∃𝑗 𝑝 = 〈𝑖, 𝑗〉)) |
26 | 24, 25 | sylibr 237 |
. . . . . 6
⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = 〈𝑖, 𝑗〉)) |
27 | | ancom 464 |
. . . . . . . 8
⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = 〈𝑖, 𝑗〉) ↔ (𝑝 = 〈𝑖, 𝑗〉 ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))) |
28 | | eleq1 2820 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑖, 𝑗〉 → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ 〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I ))) |
29 | 28 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = 〈𝑖, 𝑗〉) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ 〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I ))) |
30 | 29 | pm5.32da 582 |
. . . . . . . 8
⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ((𝑝 = 〈𝑖, 𝑗〉 ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I )) ↔ (𝑝 = 〈𝑖, 𝑗〉 ∧ 〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I )))) |
31 | 27, 30 | syl5bb 286 |
. . . . . . 7
⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = 〈𝑖, 𝑗〉) ↔ (𝑝 = 〈𝑖, 𝑗〉 ∧ 〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I )))) |
32 | 31 | 2exbidv 1930 |
. . . . . 6
⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = 〈𝑖, 𝑗〉) ↔ ∃𝑖∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ 〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I )))) |
33 | 26, 32 | mpbid 235 |
. . . . 5
⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ 〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I ))) |
34 | 28 | biimpar 481 |
. . . . . 6
⊢ ((𝑝 = 〈𝑖, 𝑗〉 ∧ 〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ I )) |
35 | 34 | exlimivv 1938 |
. . . . 5
⊢
(∃𝑖∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ 〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ I )) |
36 | 33, 35 | impbii 212 |
. . . 4
⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ∃𝑖∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ 〈𝑖, 𝑗〉 ∈ ((𝐴 × 𝐵) ∖ I ))) |
37 | | r19.42v 3253 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 (𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = 〈𝑖, 𝑗〉 ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))) |
38 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ∈ {𝑦}) |
39 | | velsn 4529 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ {𝑦} ↔ 𝑖 = 𝑦) |
40 | 38, 39 | sylib 221 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 = 𝑦) |
41 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑦 ∈ 𝐴) |
42 | 40, 41 | eqeltrd 2833 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ∈ 𝐴) |
43 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ∈ (𝐵 ∖ {𝑦})) |
44 | 43 | eldifad 3853 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ∈ 𝐵) |
45 | 43 | eldifbd 3854 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ¬ 𝑗 ∈ {𝑦}) |
46 | | velsn 4529 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ {𝑦} ↔ 𝑗 = 𝑦) |
47 | 46 | necon3bbii 2981 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑗 ∈ {𝑦} ↔ 𝑗 ≠ 𝑦) |
48 | 45, 47 | sylib 221 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ≠ 𝑦) |
49 | 48 | necomd 2989 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑦 ≠ 𝑗) |
50 | 40, 49 | eqnetrd 3001 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ≠ 𝑗) |
51 | 42, 44, 50 | jca31 518 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)) |
52 | 51 | adantll 714 |
. . . . . . . . 9
⊢
(((∃𝑥 ∈
𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ∧ 𝑦 ∈ 𝐴) ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)) |
53 | | sneq 4523 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
54 | 53 | eleq2d 2818 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑦})) |
55 | 53 | difeq2d 4011 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐵 ∖ {𝑥}) = (𝐵 ∖ {𝑦})) |
56 | 55 | eleq2d 2818 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑗 ∈ (𝐵 ∖ {𝑥}) ↔ 𝑗 ∈ (𝐵 ∖ {𝑦}))) |
57 | 54, 56 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦})))) |
58 | 57 | cbvrexvw 3349 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) |
59 | 58 | biimpi 219 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) → ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) |
60 | 52, 59 | r19.29a 3198 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)) |
61 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ∈ 𝐴) |
62 | | vsnid 4550 |
. . . . . . . . . 10
⊢ 𝑖 ∈ {𝑖} |
63 | 62 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ∈ {𝑖}) |
64 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ∈ 𝐵) |
65 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ≠ 𝑗) |
66 | 65 | necomd 2989 |
. . . . . . . . . . 11
⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ≠ 𝑖) |
67 | | velsn 4529 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ {𝑖} ↔ 𝑗 = 𝑖) |
68 | 67 | necon3bbii 2981 |
. . . . . . . . . . 11
⊢ (¬
𝑗 ∈ {𝑖} ↔ 𝑗 ≠ 𝑖) |
69 | 66, 68 | sylibr 237 |
. . . . . . . . . 10
⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → ¬ 𝑗 ∈ {𝑖}) |
70 | 64, 69 | eldifd 3852 |
. . . . . . . . 9
⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ∈ (𝐵 ∖ {𝑖})) |
71 | | sneq 4523 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑖 → {𝑥} = {𝑖}) |
72 | 71 | eleq2d 2818 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑖 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑖})) |
73 | 71 | difeq2d 4011 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑖 → (𝐵 ∖ {𝑥}) = (𝐵 ∖ {𝑖})) |
74 | 73 | eleq2d 2818 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑖 → (𝑗 ∈ (𝐵 ∖ {𝑥}) ↔ 𝑗 ∈ (𝐵 ∖ {𝑖}))) |
75 | 72, 74 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑖 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ {𝑖})))) |
76 | 75 | rspcev 3524 |
. . . . . . . . 9
⊢ ((𝑖 ∈ 𝐴 ∧ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ {𝑖}))) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) |
77 | 61, 63, 70, 76 | syl12anc 836 |
. . . . . . . 8
⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) |
78 | 60, 77 | impbii 212 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)) |
79 | 78 | anbi2i 626 |
. . . . . 6
⊢ ((𝑝 = 〈𝑖, 𝑗〉 ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = 〈𝑖, 𝑗〉 ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))) |
80 | 37, 79 | bitri 278 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 (𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = 〈𝑖, 𝑗〉 ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))) |
81 | 80 | 2exbii 1855 |
. . . 4
⊢
(∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑗(𝑝 = 〈𝑖, 𝑗〉 ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))) |
82 | 18, 36, 81 | 3bitr4i 306 |
. . 3
⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = 〈𝑖, 𝑗〉 ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))) |
83 | 6, 7, 82 | 3bitr4i 306 |
. 2
⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) ↔ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I )) |
84 | 83 | eqriv 2735 |
1
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) = ((𝐴 × 𝐵) ∖ I ) |