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→AB=CD↔A=C∧B=D∨A=D∧B=C

Proof

Step Hyp Ref Expression
1 preq1 ⊢x=A→xy=Ay
2 1 eqeq1d ⊢x=A→xy=zD↔Ay=zD
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→xy=zD↔x=z∧y=D∨x=D∧y=z↔Ay=zD↔A=z∧y=D∨A=D∧y=z
9 8 imbi2d ⊢x=A→D∈Y→xy=zD↔x=z∧y=D∨x=D∧y=z↔D∈Y→Ay=zD↔A=z∧y=D∨A=D∧y=z
10 preq2 ⊢y=B→Ay=AB
11 10 eqeq1d ⊢y=B→Ay=zD↔AB=zD
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→Ay=zD↔A=z∧y=D∨A=D∧y=z↔AB=zD↔A=z∧B=D∨A=D∧B=z
18 17 imbi2d ⊢y=B→D∈Y→Ay=zD↔A=z∧y=D∨A=D∧y=z↔D∈Y→AB=zD↔A=z∧B=D∨A=D∧B=z
19 preq1 ⊢z=C→zD=CD
20 19 eqeq2d ⊢z=C→AB=zD↔AB=CD
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→AB=zD↔A=z∧B=D∨A=D∧B=z↔AB=CD↔A=C∧B=D∨A=D∧B=C
27 26 imbi2d ⊢z=C→D∈Y→AB=zD↔A=z∧B=D∨A=D∧B=z↔D∈Y→AB=CD↔A=C∧B=D∨A=D∧B=C
28 preq2 ⊢w=D→zw=zD
29 28 eqeq2d ⊢w=D→xy=zw↔xy=zD
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 ⊢xy=zw↔x=z∧y=w∨x=w∧y=z
40 29 34 39 vtoclbg ⊢D∈Y→xy=zD↔x=z∧y=D∨x=D∧y=z
41 40 a1i ⊢x∈V∧y∈W∧z∈X→D∈Y→xy=zD↔x=z∧y=D∨x=D∧y=z
42 9 18 27 41 vtocl3ga ⊢A∈V∧B∈W∧C∈X→D∈Y→AB=CD↔A=C∧B=D∨A=D∧B=C
43 42 3expa ⊢A∈V∧B∈W∧C∈X→D∈Y→AB=CD↔A=C∧B=D∨A=D∧B=C
44 43 impr ⊢A∈V∧B∈W∧C∈X∧D∈Y→AB=CD↔A=C∧B=D∨A=D∧B=C