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 e. C /\ B e. C ) -> { A , B } C_ C )

Proof

Step Hyp Ref Expression
1 prssg 
 |-  ( ( A e. C /\ B e. C ) -> ( ( A e. C /\ B e. C ) <-> { A , B } C_ C ) )
2 1 ibi 
 |-  ( ( A e. C /\ B e. C ) -> { A , B } C_ C )