Theorem prprc

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

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

Proof

Step	Hyp	Ref	Expression
1		prprc1	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 , 𝐵 } = { 𝐵 } )
2		snprc	⊢ ( ¬ 𝐵 ∈ V ↔ { 𝐵 } = ∅ )
3	2	biimpi	⊢ ( ¬ 𝐵 ∈ V → { 𝐵 } = ∅ )
4	1 3	sylan9eq	⊢ ( ( ¬ 𝐴 ∈ V ∧ ¬ 𝐵 ∈ V ) → { 𝐴 , 𝐵 } = ∅ )