Theorem ssbrd 5129

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

Hypothesis

Ref	Expression
ssbrd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
ssbrd	⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))

Proof of Theorem ssbrd

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  ⟨cop 4574   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3907  df-br 5087

This theorem is referenced by:  ssbr  5130  sess1  5589  brrelex12  5676  eqbrrdva  5818  predtrss  6280  ersym  8649  ertr  8652  ttrclss  9632  fpwwe2lem5  10549  fpwwe2lem6  10550  fpwwe2lem8  10552  fpwwe2lem11  10555  fpwwe2lem12  10556  fpwwe2  10557  coss12d  14925  fthres2  17892  invfuc  17935  pospo  18300  dirref  18558  efgcpbl  19722  frgpuplem  19738  subrguss  20555  znleval  21544  ustref  24194  ustuqtop4  24219  metider  34054  mclsppslem  35781  fundmpss  35965  eqvrelsym  39024  eqvreltr  39026  iunrelexpuztr  44164  frege96d  44194  frege91d  44196  frege98d  44198  frege124d  44206  grucollcld  44705