# Metamath Proof Explorer

## Theorem prneprprc

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

Ref Expression
Assertion prneprprc ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\wedge ¬{C}\in \mathrm{V}\right)\to \left\{{A},{B}\right\}\ne \left\{{C},{D}\right\}$

### Proof

Step Hyp Ref Expression
1 prnesn ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\to \left\{{A},{B}\right\}\ne \left\{{D}\right\}$
2 1 adantr ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\wedge ¬{C}\in \mathrm{V}\right)\to \left\{{A},{B}\right\}\ne \left\{{D}\right\}$
3 prprc1 ${⊢}¬{C}\in \mathrm{V}\to \left\{{C},{D}\right\}=\left\{{D}\right\}$
4 3 neeq2d ${⊢}¬{C}\in \mathrm{V}\to \left(\left\{{A},{B}\right\}\ne \left\{{C},{D}\right\}↔\left\{{A},{B}\right\}\ne \left\{{D}\right\}\right)$
5 4 adantl ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\wedge ¬{C}\in \mathrm{V}\right)\to \left(\left\{{A},{B}\right\}\ne \left\{{C},{D}\right\}↔\left\{{A},{B}\right\}\ne \left\{{D}\right\}\right)$
6 2 5 mpbird ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\wedge ¬{C}\in \mathrm{V}\right)\to \left\{{A},{B}\right\}\ne \left\{{C},{D}\right\}$