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 ) |
| 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 ) |