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 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )