This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem preq12bg

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

Ref Expression
Assertion preq12bg 
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. 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 e. Y -> ( { x , y } = { z , D } <-> ( ( x = z /\ y = D ) \/ ( x = D /\ y = z ) ) ) ) <-> ( D e. 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 e. Y -> ( { A , y } = { z , D } <-> ( ( A = z /\ y = D ) \/ ( A = D /\ y = z ) ) ) ) <-> ( D e. 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 e. Y -> ( { A , B } = { z , D } <-> ( ( A = z /\ B = D ) \/ ( A = D /\ B = z ) ) ) ) <-> ( D e. 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 e. _V
36 vex 
 |-  y e. _V
37 vex 
 |-  z e. _V
38 vex 
 |-  w e. _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 e. Y -> ( { x , y } = { z , D } <-> ( ( x = z /\ y = D ) \/ ( x = D /\ y = z ) ) ) )
41 40 a1i 
 |-  ( ( x e. V /\ y e. W /\ z e. X ) -> ( D e. Y -> ( { x , y } = { z , D } <-> ( ( x = z /\ y = D ) \/ ( x = D /\ y = z ) ) ) ) )
42 9 18 27 41 vtocl3ga 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( D e. Y -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) ) )
43 42 3expa 
 |-  ( ( ( A e. V /\ B e. W ) /\ C e. X ) -> ( D e. Y -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) ) )
44 43 impr 
 |-  ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )