Theorem prprc1

Description: A proper class vanishes in an unordered pair. (Contributed by NM, 15-Jul-1993)

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

Proof

Step	Hyp	Ref	Expression
1		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
2		uneq1	⊢ ( { 𝐴 } = ∅ → ( { 𝐴 } ∪ { 𝐵 } ) = ( ∅ ∪ { 𝐵 } ) )
3		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
4		uncom	⊢ ( ∅ ∪ { 𝐵 } ) = ( { 𝐵 } ∪ ∅ )
5		un0	⊢ ( { 𝐵 } ∪ ∅ ) = { 𝐵 }
6	4 5	eqtr2i	⊢ { 𝐵 } = ( ∅ ∪ { 𝐵 } )
7	2 3 6	3eqtr4g	⊢ ( { 𝐴 } = ∅ → { 𝐴 , 𝐵 } = { 𝐵 } )
8	1 7	sylbi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 , 𝐵 } = { 𝐵 } )