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⟩\setminus \left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		0nelop	$$⊢\neg \varnothing \in ⟨X,Y⟩$$
2		disjsn	$$⊢⟨X,Y⟩\cap \left\{\varnothing \right\}=\varnothing \leftrightarrow \neg \varnothing \in ⟨X,Y⟩$$
3	1 2	mpbir	$$⊢⟨X,Y⟩\cap \left\{\varnothing \right\}=\varnothing$$
4		disjdif2	$$⊢⟨X,Y⟩\cap \left\{\varnothing \right\}=\varnothing \to ⟨X,Y⟩\setminus \left\{\varnothing \right\}=⟨X,Y⟩$$
5	3 4	ax-mp	$$⊢⟨X,Y⟩\setminus \left\{\varnothing \right\}=⟨X,Y⟩$$
6	5	eqcomi	$$⊢⟨X,Y⟩=⟨X,Y⟩\setminus \left\{\varnothing \right\}$$