Metamath Proof Explorer


Theorem prss

Description: A pair of elements of a class is a subset of the class. Theorem 7.5 of Quine p. 49. (Contributed by NM, 30-May-1994) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by JJ, 23-Jul-2021)

Ref Expression
Hypotheses prss.1
|- A e. _V
prss.2
|- B e. _V
Assertion prss
|- ( ( A e. C /\ B e. C ) <-> { A , B } C_ C )

Proof

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