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

Metamath Proof Explorer

Theorem prprc2

Description: A proper class vanishes in an unordered pair. (Contributed by NM, 22-Mar-2006)

Ref Expression
Assertion prprc2 ⊢ ¬ B ∈ V → A B = A

Proof

Step Hyp Ref Expression
1 prcom ⊢ A B = B A
2 prprc1 ⊢ ¬ B ∈ V → B A = A
3 1 2 eqtrid ⊢ ¬ B ∈ V → A B = A