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 ↔ M N = 2

Proof

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