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	⊢ ⟨ 𝑋 , 𝑌 ⟩ = ( ⟨ 𝑋 , 𝑌 ⟩ ∖ { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		0nelop	⊢ ¬ ∅ ∈ ⟨ 𝑋 , 𝑌 ⟩
2		disjsn	⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ∩ { ∅ } ) = ∅ ↔ ¬ ∅ ∈ ⟨ 𝑋 , 𝑌 ⟩ )
3	1 2	mpbir	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∩ { ∅ } ) = ∅
4		disjdif2	⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ∩ { ∅ } ) = ∅ → ( ⟨ 𝑋 , 𝑌 ⟩ ∖ { ∅ } ) = ⟨ 𝑋 , 𝑌 ⟩ )
5	3 4	ax-mp	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∖ { ∅ } ) = ⟨ 𝑋 , 𝑌 ⟩
6	5	eqcomi	⊢ ⟨ 𝑋 , 𝑌 ⟩ = ( ⟨ 𝑋 , 𝑌 ⟩ ∖ { ∅ } )