# Metamath Proof Explorer

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 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left({A}\in {C}\wedge {B}\in {C}\right)↔\left\{{A},{B}\right\}\subseteq {C}\right)$

### Proof

Step Hyp Ref Expression
1 snssg ${⊢}{A}\in {V}\to \left({A}\in {C}↔\left\{{A}\right\}\subseteq {C}\right)$
2 snssg ${⊢}{B}\in {W}\to \left({B}\in {C}↔\left\{{B}\right\}\subseteq {C}\right)$
3 1 2 bi2anan9 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left({A}\in {C}\wedge {B}\in {C}\right)↔\left(\left\{{A}\right\}\subseteq {C}\wedge \left\{{B}\right\}\subseteq {C}\right)\right)$
4 unss ${⊢}\left(\left\{{A}\right\}\subseteq {C}\wedge \left\{{B}\right\}\subseteq {C}\right)↔\left\{{A}\right\}\cup \left\{{B}\right\}\subseteq {C}$
5 df-pr ${⊢}\left\{{A},{B}\right\}=\left\{{A}\right\}\cup \left\{{B}\right\}$
6 5 sseq1i ${⊢}\left\{{A},{B}\right\}\subseteq {C}↔\left\{{A}\right\}\cup \left\{{B}\right\}\subseteq {C}$
7 4 6 bitr4i ${⊢}\left(\left\{{A}\right\}\subseteq {C}\wedge \left\{{B}\right\}\subseteq {C}\right)↔\left\{{A},{B}\right\}\subseteq {C}$
8 3 7 syl6bb ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left({A}\in {C}\wedge {B}\in {C}\right)↔\left\{{A},{B}\right\}\subseteq {C}\right)$