Metamath Proof Explorer

Theorem ssprss

Description: A pair as subset of a pair. (Contributed by AV, 26-Oct-2020)

Ref Expression
Assertion ssprss ⊢ A ∈ V ∧ B ∈ W → A B ⊆ C D ↔ A = C ∨ A = D ∧ B = C ∨ B = D

Proof

Step Hyp Ref Expression
1 prssg ⊢ A ∈ V ∧ B ∈ W → A ∈ C D ∧ B ∈ C D ↔ A B ⊆ C D
2 elprg ⊢ A ∈ V → A ∈ C D ↔ A = C ∨ A = D
3 elprg ⊢ B ∈ W → B ∈ C D ↔ B = C ∨ B = D
4 2 3 bi2anan9 ⊢ A ∈ V ∧ B ∈ W → A ∈ C D ∧ B ∈ C D ↔ A = C ∨ A = D ∧ B = C ∨ B = D
5 1 4 bitr3d ⊢ A ∈ V ∧ B ∈ W → A B ⊆ C D ↔ A = C ∨ A = D ∧ B = C ∨ B = D