Metamath Proof Explorer

Theorem hashprb

Description: The size of an unordered pair is 2 if and only if its elements are different sets. (Contributed by Alexander van der Vekens, 17-Jan-2018)

Ref Expression
Assertion hashprb ⊢M∈V∧N∈V∧M≠N↔MN=2

Proof

Step Hyp Ref Expression
1 hashprg ⊢M∈V∧N∈V→M≠N↔MN=2
2 1 biimp3a ⊢M∈V∧N∈V∧M≠N→MN=2
3 elprchashprn2 ⊢¬M∈V→¬MN=2
4 pm2.21 ⊢¬MN=2→MN=2→M∈V∧N∈V∧M≠N
5 3 4 syl ⊢¬M∈V→MN=2→M∈V∧N∈V∧M≠N
6 elprchashprn2 ⊢¬N∈V→¬NM=2
7 prcom ⊢NM=MN
8 7 fveq2i ⊢NM=MN
9 8 eqeq1i ⊢NM=2↔MN=2
10 9 4 sylnbi ⊢¬NM=2→MN=2→M∈V∧N∈V∧M≠N
11 6 10 syl ⊢¬N∈V→MN=2→M∈V∧N∈V∧M≠N
12 simpll ⊢M∈V∧N∈V∧MN=2→M∈V
13 simplr ⊢M∈V∧N∈V∧MN=2→N∈V
14 1 biimpar ⊢M∈V∧N∈V∧MN=2→M≠N
15 12 13 14 3jca ⊢M∈V∧N∈V∧MN=2→M∈V∧N∈V∧M≠N
16 15 ex ⊢M∈V∧N∈V→MN=2→M∈V∧N∈V∧M≠N
17 5 11 16 ecase ⊢MN=2→M∈V∧N∈V∧M≠N
18 2 17 impbii ⊢M∈V∧N∈V∧M≠N↔MN=2