Metamath Proof Explorer


Theorem prssi

Description: A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015)

Ref Expression
Assertion prssi ⊢ A ∈ C ∧ B ∈ C → A B ⊆ C

Proof

Step Hyp Ref Expression
1 prssg ⊢ A ∈ C ∧ B ∈ C → A ∈ C ∧ B ∈ C ↔ A B ⊆ C
2 1 ibi ⊢ A ∈ C ∧ B ∈ C → A B ⊆ C