Theorem prprc2

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

	Ref	Expression
Assertion	prprc2	⊢ ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } = { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		prcom	⊢ { 𝐴 , 𝐵 } = { 𝐵 , 𝐴 }
2		prprc1	⊢ ( ¬ 𝐵 ∈ V → { 𝐵 , 𝐴 } = { 𝐴 } )
3	1 2	eqtrid	⊢ ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } = { 𝐴 } )