Theorem ssprss

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

	Ref	Expression
Assertion	ssprss	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		prssg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∈ { 𝐶 , 𝐷 } ∧ 𝐵 ∈ { 𝐶 , 𝐷 } ) ↔ { 𝐴 , 𝐵 } ⊆ { 𝐶 , 𝐷 } ) )
2		elprg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ) )
3		elprg	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ∈ { 𝐶 , 𝐷 } ↔ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) )
4	2 3	bi2anan9	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∈ { 𝐶 , 𝐷 } ∧ 𝐵 ∈ { 𝐶 , 𝐷 } ) ↔ ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) ) )
5	1 4	bitr3d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 , 𝐵 } ⊆ { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∨ 𝐴 = 𝐷 ) ∧ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐷 ) ) ) )