Metamath Proof Explorer

Theorem hashprdifel

Description: The elements of an unordered pair of size 2 are different sets. (Contributed by AV, 27-Jan-2020)

Ref Expression
Hypothesis hashprdifel.s ⊢ S = A B
Assertion hashprdifel ⊢ S = 2 → A ∈ S ∧ B ∈ S ∧ A ≠ B

Proof

Step Hyp Ref Expression
1 hashprdifel.s ⊢ S = A B
2 1 fveq2i ⊢ S = A B
3 2 eqeq1i ⊢ S = 2 ↔ A B = 2
4 hashprb ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B ↔ A B = 2
5 3 4 bitr4i ⊢ S = 2 ↔ A ∈ V ∧ B ∈ V ∧ A ≠ B
6 prid1g ⊢ A ∈ V → A ∈ A B
7 6 3ad2ant1 ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B → A ∈ A B
8 7 1 eleqtrrdi ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B → A ∈ S
9 prid2g ⊢ B ∈ V → B ∈ A B
10 9 3ad2ant2 ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B → B ∈ A B
11 10 1 eleqtrrdi ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B → B ∈ S
12 simp3 ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B → A ≠ B
13 8 11 12 3jca ⊢ A ∈ V ∧ B ∈ V ∧ A ≠ B → A ∈ S ∧ B ∈ S ∧ A ≠ B
14 5 13 sylbi ⊢ S = 2 → A ∈ S ∧ B ∈ S ∧ A ≠ B