Metamath Proof Explorer

Theorem prnesn

Description: A proper unordered pair is not a (proper or improper) singleton. (Contributed by AV, 13-Jun-2022)

Ref Expression
Assertion prnesn ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ≠ C

Proof

Step Hyp Ref Expression
1 eqtr3 ⊢ A = C ∧ B = C → A = B
2 1 necon3ai ⊢ A ≠ B → ¬ A = C ∧ B = C
3 2 3ad2ant3 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → ¬ A = C ∧ B = C
4 simp1 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A ∈ V
5 simp2 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → B ∈ W
6 4 5 preqsnd ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C ↔ A = C ∧ B = C
7 6 necon3abid ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ≠ C ↔ ¬ A = C ∧ B = C
8 3 7 mpbird ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ≠ C