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 V
prss.2 B V
Assertion prss A C B C A B C


Step Hyp Ref Expression
1 prss.1 A V
2 prss.2 B V
3 prssg A V B V A C B C A B C
4 1 2 3 mp2an A C B C A B C