Theorem ssbrd

Description: Deduction from a subclass relationship of binary relations. (Contributed by NM, 30-Apr-2004)

	Ref	Expression
Hypothesis	ssbrd.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion	ssbrd	⊢ ( 𝜑 → ( 𝐶 𝐴 𝐷 → 𝐶 𝐵 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		ssbrd.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2	1	sseld	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝐴 → ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝐵 ) )
3		df-br	⊢ ( 𝐶 𝐴 𝐷 ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝐴 )
4		df-br	⊢ ( 𝐶 𝐵 𝐷 ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝐵 )
5	2 3 4	3imtr4g	⊢ ( 𝜑 → ( 𝐶 𝐴 𝐷 → 𝐶 𝐵 𝐷 ) )