This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ ¬ C ∈ V → A B ≠ C D

Proof

Step Hyp Ref Expression
1 prnesn ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ≠ D
2 1 adantr ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ ¬ C ∈ V → A B ≠ D
3 prprc1 ⊢ ¬ C ∈ V → C D = D
4 3 neeq2d ⊢ ¬ C ∈ V → A B ≠ C D ↔ A B ≠ D
5 4 adantl ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ ¬ C ∈ V → A B ≠ C D ↔ A B ≠ D
6 2 5 mpbird ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ ¬ C ∈ V → A B ≠ C D