| Step | Hyp | Ref
| Expression |
| 1 | | preq1 4733 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → {𝑥, 𝑦} = {𝐴, 𝑦}) |
| 2 | 1 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝑦} = {𝑧, 𝐷})) |
| 3 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 = 𝑧 ↔ 𝐴 = 𝑧)) |
| 4 | 3 | anbi1d 631 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝑧 ∧ 𝑦 = 𝐷))) |
| 5 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 = 𝐷 ↔ 𝐴 = 𝐷)) |
| 6 | 5 | anbi1d 631 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐷 ∧ 𝑦 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))) |
| 7 | 4, 6 | orbi12d 919 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))) |
| 8 | 2, 7 | bibi12d 345 |
. . . . 5
⊢ (𝑥 = 𝐴 → (({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))) ↔ ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))))) |
| 9 | 8 | imbi2d 340 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))))) |
| 10 | | preq2 4734 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → {𝐴, 𝑦} = {𝐴, 𝐵}) |
| 11 | 10 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝑧, 𝐷})) |
| 12 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝑦 = 𝐷 ↔ 𝐵 = 𝐷)) |
| 13 | 12 | anbi2d 630 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝑧 ∧ 𝐵 = 𝐷))) |
| 14 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝑦 = 𝑧 ↔ 𝐵 = 𝑧)) |
| 15 | 14 | anbi2d 630 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → ((𝐴 = 𝐷 ∧ 𝑦 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))) |
| 16 | 13, 15 | orbi12d 919 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)) ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))) |
| 17 | 11, 16 | bibi12d 345 |
. . . . 5
⊢ (𝑦 = 𝐵 → (({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))))) |
| 18 | 17 | imbi2d 340 |
. . . 4
⊢ (𝑦 = 𝐵 → ((𝐷 ∈ 𝑌 → ({𝐴, 𝑦} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝑦 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))))) |
| 19 | | preq1 4733 |
. . . . . . 7
⊢ (𝑧 = 𝐶 → {𝑧, 𝐷} = {𝐶, 𝐷}) |
| 20 | 19 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑧 = 𝐶 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ {𝐴, 𝐵} = {𝐶, 𝐷})) |
| 21 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑧 = 𝐶 → (𝐴 = 𝑧 ↔ 𝐴 = 𝐶)) |
| 22 | 21 | anbi1d 631 |
. . . . . . 7
⊢ (𝑧 = 𝐶 → ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
| 23 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑧 = 𝐶 → (𝐵 = 𝑧 ↔ 𝐵 = 𝐶)) |
| 24 | 23 | anbi2d 630 |
. . . . . . 7
⊢ (𝑧 = 𝐶 → ((𝐴 = 𝐷 ∧ 𝐵 = 𝑧) ↔ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) |
| 25 | 22, 24 | orbi12d 919 |
. . . . . 6
⊢ (𝑧 = 𝐶 → (((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)) ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
| 26 | 20, 25 | bibi12d 345 |
. . . . 5
⊢ (𝑧 = 𝐶 → (({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧))) ↔ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))) |
| 27 | 26 | imbi2d 340 |
. . . 4
⊢ (𝑧 = 𝐶 → ((𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝑧, 𝐷} ↔ ((𝐴 = 𝑧 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝑧)))) ↔ (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))))) |
| 28 | | preq2 4734 |
. . . . . . 7
⊢ (𝑤 = 𝐷 → {𝑧, 𝑤} = {𝑧, 𝐷}) |
| 29 | 28 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑤 = 𝐷 → ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ {𝑥, 𝑦} = {𝑧, 𝐷})) |
| 30 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑤 = 𝐷 → (𝑦 = 𝑤 ↔ 𝑦 = 𝐷)) |
| 31 | 30 | anbi2d 630 |
. . . . . . 7
⊢ (𝑤 = 𝐷 → ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ↔ (𝑥 = 𝑧 ∧ 𝑦 = 𝐷))) |
| 32 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑤 = 𝐷 → (𝑥 = 𝑤 ↔ 𝑥 = 𝐷)) |
| 33 | 32 | anbi1d 631 |
. . . . . . 7
⊢ (𝑤 = 𝐷 → ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) ↔ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))) |
| 34 | 31, 33 | orbi12d 919 |
. . . . . 6
⊢ (𝑤 = 𝐷 → (((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∨ (𝑥 = 𝑤 ∧ 𝑦 = 𝑧)) ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))) |
| 35 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 36 | | vex 3484 |
. . . . . . 7
⊢ 𝑦 ∈ V |
| 37 | | vex 3484 |
. . . . . . 7
⊢ 𝑧 ∈ V |
| 38 | | vex 3484 |
. . . . . . 7
⊢ 𝑤 ∈ V |
| 39 | 35, 36, 37, 38 | preq12b 4850 |
. . . . . 6
⊢ ({𝑥, 𝑦} = {𝑧, 𝑤} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∨ (𝑥 = 𝑤 ∧ 𝑦 = 𝑧))) |
| 40 | 29, 34, 39 | vtoclbg 3557 |
. . . . 5
⊢ (𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧)))) |
| 41 | 40 | a1i 11 |
. . . 4
⊢ ((𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ∧ 𝑧 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝑥, 𝑦} = {𝑧, 𝐷} ↔ ((𝑥 = 𝑧 ∧ 𝑦 = 𝐷) ∨ (𝑥 = 𝐷 ∧ 𝑦 = 𝑧))))) |
| 42 | 9, 18, 27, 41 | vtocl3ga 3583 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))) |
| 43 | 42 | 3expa 1119 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐶 ∈ 𝑋) → (𝐷 ∈ 𝑌 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))))) |
| 44 | 43 | impr 454 |
1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |