# 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 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left\{{A},{B}\right\}\ne \left\{{C}\right\}$

### Proof

Step Hyp Ref Expression
1 eqtr3 ${⊢}\left({A}={C}\wedge {B}={C}\right)\to {A}={B}$
2 1 necon3ai ${⊢}{A}\ne {B}\to ¬\left({A}={C}\wedge {B}={C}\right)$
3 2 3ad2ant3 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to ¬\left({A}={C}\wedge {B}={C}\right)$
4 elex ${⊢}{A}\in {V}\to {A}\in \mathrm{V}$
5 4 3ad2ant1 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to {A}\in \mathrm{V}$
6 elex ${⊢}{B}\in {W}\to {B}\in \mathrm{V}$
7 6 3ad2ant2 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to {B}\in \mathrm{V}$
8 5 7 preqsnd ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left(\left\{{A},{B}\right\}=\left\{{C}\right\}↔\left({A}={C}\wedge {B}={C}\right)\right)$
9 8 necon3abid ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left(\left\{{A},{B}\right\}\ne \left\{{C}\right\}↔¬\left({A}={C}\wedge {B}={C}\right)\right)$
10 3 9 mpbird ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left\{{A},{B}\right\}\ne \left\{{C}\right\}$