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 e. _V -> { A , B } = { A } )

Proof

Step Hyp Ref Expression
1 prcom 
 |-  { A , B } = { B , A }
2 prprc1 
 |-  ( -. B e. _V -> { B , A } = { A } )
3 1 2 eqtrid 
 |-  ( -. B e. _V -> { A , B } = { A } )