Metamath Proof Explorer


Theorem prssg

Description: A pair of elements of a class is a subset of the class. Theorem 7.5 of Quine p. 49. (Contributed by NM, 22-Mar-2006) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion prssg AVBWACBCABC

Proof

Step Hyp Ref Expression
1 snssg AVACAC
2 snssg BWBCBC
3 1 2 bi2anan9 AVBWACBCACBC
4 unss ACBCABC
5 df-pr AB=AB
6 5 sseq1i ABCABC
7 4 6 bitr4i ACBCABC
8 3 7 bitrdi AVBWACBCABC