Step |
Hyp |
Ref |
Expression |
1 |
|
preleq.b |
⊢ 𝐵 ∈ V |
2 |
|
preleqALT.d |
⊢ 𝐷 ∈ V |
3 |
1
|
jctr |
⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V ) ) |
4 |
2
|
jctr |
⊢ ( 𝐶 ∈ 𝐷 → ( 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ V ) ) |
5 |
|
preq12bg |
⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ V ) ∧ ( 𝐶 ∈ 𝐷 ∧ 𝐷 ∈ V ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) ) |
6 |
3 4 5
|
syl2an |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) ) |
7 |
6
|
biimpa |
⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) |
8 |
7
|
ord |
⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( ¬ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) |
9 |
|
en2lp |
⊢ ¬ ( 𝐷 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ) |
10 |
|
eleq12 |
⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 ∈ 𝐵 ↔ 𝐷 ∈ 𝐶 ) ) |
11 |
10
|
anbi1d |
⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) ↔ ( 𝐷 ∈ 𝐶 ∧ 𝐶 ∈ 𝐷 ) ) ) |
12 |
9 11
|
mtbiri |
⊢ ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) ) |
13 |
8 12
|
syl6 |
⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( ¬ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) ) ) |
14 |
13
|
con4d |
⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) |
15 |
14
|
ex |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) ) |
16 |
15
|
pm2.43a |
⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) |
17 |
16
|
imp |
⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) |