Metamath Proof Explorer


Theorem preq12bg

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

Ref Expression
Assertion preq12bg ( ( ( 𝐴𝑉𝐵𝑊 ) ∧ ( 𝐶𝑋𝐷𝑌 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) ) )

Proof

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