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