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 ⊢ A ∈ V ∧ B ∈ W → A ∈ C ∧ B ∈ C ↔ A B ⊆ C

Proof

Step Hyp Ref Expression
1 snssg ⊢ A ∈ V → A ∈ C ↔ A ⊆ C
2 snssg ⊢ B ∈ W → B ∈ C ↔ B ⊆ C
3 1 2 bi2anan9 ⊢ A ∈ V ∧ B ∈ W → A ∈ C ∧ B ∈ C ↔ A ⊆ C ∧ B ⊆ C
4 unss ⊢ A ⊆ C ∧ B ⊆ C ↔ A ∪ B ⊆ C
5 df-pr ⊢ A B = A ∪ B
6 5 sseq1i ⊢ A B ⊆ C ↔ A ∪ B ⊆ C
7 4 6 bitr4i ⊢ A ⊆ C ∧ B ⊆ C ↔ A B ⊆ C
8 3 7 bitrdi ⊢ A ∈ V ∧ B ∈ W → A ∈ C ∧ B ∈ C ↔ A B ⊆ C