Theorem prneprprc

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

	Ref	Expression
Assertion	prneprprc	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ¬ 𝐶 ∈ V ) → { 𝐴 , 𝐵 } ≠ { 𝐶 , 𝐷 } )

Proof

Step	Hyp	Ref	Expression
1		prnesn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≠ { 𝐷 } )
2	1	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ¬ 𝐶 ∈ V ) → { 𝐴 , 𝐵 } ≠ { 𝐷 } )
3		prprc1	⊢ ( ¬ 𝐶 ∈ V → { 𝐶 , 𝐷 } = { 𝐷 } )
4	3	neeq2d	⊢ ( ¬ 𝐶 ∈ V → ( { 𝐴 , 𝐵 } ≠ { 𝐶 , 𝐷 } ↔ { 𝐴 , 𝐵 } ≠ { 𝐷 } ) )
5	4	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ¬ 𝐶 ∈ V ) → ( { 𝐴 , 𝐵 } ≠ { 𝐶 , 𝐷 } ↔ { 𝐴 , 𝐵 } ≠ { 𝐷 } ) )
6	2 5	mpbird	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ ¬ 𝐶 ∈ V ) → { 𝐴 , 𝐵 } ≠ { 𝐶 , 𝐷 } )