Theorem opwo0id

Description: An ordered pair is equal to the ordered pair without the empty set. This is because no ordered pair contains the empty set. (Contributed by AV, 15-Nov-2021)

	Ref	Expression
Assertion	opwo0id	|- <. X , Y >. = ( <. X , Y >. \ { (/) } )

Proof

Step	Hyp	Ref	Expression
1		0nelop	|- -. (/) e. <. X , Y >.
2		disjsn	|- ( ( <. X , Y >. i^i { (/) } ) = (/) <-> -. (/) e. <. X , Y >. )
3	1 2	mpbir	|- ( <. X , Y >. i^i { (/) } ) = (/)
4		disjdif2	|- ( ( <. X , Y >. i^i { (/) } ) = (/) -> ( <. X , Y >. \ { (/) } ) = <. X , Y >. )
5	3 4	ax-mp	|- ( <. X , Y >. \ { (/) } ) = <. X , Y >.
6	5	eqcomi	|- <. X , Y >. = ( <. X , Y >. \ { (/) } )