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 elex ⊢ A ∈ V → A ∈ V
5 4 3ad2ant1 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A ∈ V
6 elex ⊢ B ∈ W → B ∈ V
7 6 3ad2ant2 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → B ∈ V
8 5 7 preqsnd ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C ↔ A = C ∧ B = C
9 8 necon3abid ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ≠ C ↔ ¬ A = C ∧ B = C
10 3 9 mpbird ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ≠ C