Metamath Proof Explorer

Theorem preq12bg

Description: Closed form of preq12b . (Contributed by Scott Fenton, 28-Mar-2014)

Ref Expression
Assertion preq12bg ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X ∧ D ∈ Y → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C

Proof

Step Hyp Ref Expression
1 preq1 ⊢ x = A → x y = A y
2 1 eqeq1d ⊢ x = A → x y = z D ↔ A y = z D
3 eqeq1 ⊢ x = A → x = z ↔ A = z
4 3 anbi1d ⊢ x = A → x = z ∧ y = D ↔ A = z ∧ y = D
5 eqeq1 ⊢ x = A → x = D ↔ A = D
6 5 anbi1d ⊢ x = A → x = D ∧ y = z ↔ A = D ∧ y = z
7 4 6 orbi12d ⊢ x = A → x = z ∧ y = D ∨ x = D ∧ y = z ↔ A = z ∧ y = D ∨ A = D ∧ y = z
8 2 7 bibi12d ⊢ x = A → x y = z D ↔ x = z ∧ y = D ∨ x = D ∧ y = z ↔ A y = z D ↔ A = z ∧ y = D ∨ A = D ∧ y = z
9 8 imbi2d ⊢ x = A → D ∈ Y → x y = z D ↔ x = z ∧ y = D ∨ x = D ∧ y = z ↔ D ∈ Y → A y = z D ↔ A = z ∧ y = D ∨ A = D ∧ y = z
10 preq2 ⊢ y = B → A y = A B
11 10 eqeq1d ⊢ y = B → A y = z D ↔ A B = z D
12 eqeq1 ⊢ y = B → y = D ↔ B = D
13 12 anbi2d ⊢ y = B → A = z ∧ y = D ↔ A = z ∧ B = D
14 eqeq1 ⊢ y = B → y = z ↔ B = z
15 14 anbi2d ⊢ y = B → A = D ∧ y = z ↔ A = D ∧ B = z
16 13 15 orbi12d ⊢ y = B → A = z ∧ y = D ∨ A = D ∧ y = z ↔ A = z ∧ B = D ∨ A = D ∧ B = z
17 11 16 bibi12d ⊢ y = B → A y = z D ↔ A = z ∧ y = D ∨ A = D ∧ y = z ↔ A B = z D ↔ A = z ∧ B = D ∨ A = D ∧ B = z
18 17 imbi2d ⊢ y = B → D ∈ Y → A y = z D ↔ A = z ∧ y = D ∨ A = D ∧ y = z ↔ D ∈ Y → A B = z D ↔ A = z ∧ B = D ∨ A = D ∧ B = z
19 preq1 ⊢ z = C → z D = C D
20 19 eqeq2d ⊢ z = C → A B = z D ↔ A B = C D
21 eqeq2 ⊢ z = C → A = z ↔ A = C
22 21 anbi1d ⊢ z = C → A = z ∧ B = D ↔ A = C ∧ B = D
23 eqeq2 ⊢ z = C → B = z ↔ B = C
24 23 anbi2d ⊢ z = C → A = D ∧ B = z ↔ A = D ∧ B = C
25 22 24 orbi12d ⊢ z = C → A = z ∧ B = D ∨ A = D ∧ B = z ↔ A = C ∧ B = D ∨ A = D ∧ B = C
26 20 25 bibi12d ⊢ z = C → A B = z D ↔ A = z ∧ B = D ∨ A = D ∧ B = z ↔ A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
27 26 imbi2d ⊢ z = C → D ∈ Y → A B = z D ↔ A = z ∧ B = D ∨ A = D ∧ B = z ↔ D ∈ Y → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
28 preq2 ⊢ w = D → z w = z D
29 28 eqeq2d ⊢ w = D → x y = z w ↔ x y = z D
30 eqeq2 ⊢ w = D → y = w ↔ y = D
31 30 anbi2d ⊢ w = D → x = z ∧ y = w ↔ x = z ∧ y = D
32 eqeq2 ⊢ w = D → x = w ↔ x = D
33 32 anbi1d ⊢ w = D → x = w ∧ y = z ↔ x = D ∧ y = z
34 31 33 orbi12d ⊢ w = D → x = z ∧ y = w ∨ x = w ∧ y = z ↔ x = z ∧ y = D ∨ x = D ∧ y = z
35 vex ⊢ x ∈ V
36 vex ⊢ y ∈ V
37 vex ⊢ z ∈ V
38 vex ⊢ w ∈ V
39 35 36 37 38 preq12b ⊢ x y = z w ↔ x = z ∧ y = w ∨ x = w ∧ y = z
40 29 34 39 vtoclbg ⊢ D ∈ Y → x y = z D ↔ x = z ∧ y = D ∨ x = D ∧ y = z
41 40 a1i ⊢ x ∈ V ∧ y ∈ W ∧ z ∈ X → D ∈ Y → x y = z D ↔ x = z ∧ y = D ∨ x = D ∧ y = z
42 9 18 27 41 vtocl3ga ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → D ∈ Y → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
43 42 3expa ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → D ∈ Y → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
44 43 impr ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X ∧ D ∈ Y → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C