Metamath Proof Explorer

Theorem prprc

Description: An unordered pair containing two proper classes is the empty set. (Contributed by NM, 22-Mar-2006)

Ref Expression
Assertion prprc 
|- ( ( -. A e. _V /\ -. B e. _V ) -> { A , B } = (/) )

Proof

Step Hyp Ref Expression
1 prprc1 
 |-  ( -. A e. _V -> { A , B } = { B } )
2 snprc 
 |-  ( -. B e. _V <-> { B } = (/) )
3 2 biimpi 
 |-  ( -. B e. _V -> { B } = (/) )
4 1 3 sylan9eq 
 |-  ( ( -. A e. _V /\ -. B e. _V ) -> { A , B } = (/) )