Metamath Proof Explorer


Theorem 0in

Description: The intersection of the empty set with a class is the empty set. Commuted form of 0in . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion 0in ⊢ ∅ ∩ A = ∅

Proof

Step Hyp Ref Expression
1 in0 ⊢ A ∩ ∅ = ∅
2 1 ineqcomi ⊢ ∅ ∩ A = ∅