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

Proof

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