Theorem ssbrd 5148

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 3930	. 2 ⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∈ 𝐴 → ⟨𝐶, 𝐷⟩ ∈ 𝐵))
3		df-br 5104	. 2 ⊢ (𝐶𝐴𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐴)
4		df-br 5104	. 2 ⊢ (𝐶𝐵𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ 𝐵)
5	2, 3, 4	3imtr4g 299	1 ⊢ (𝜑 → (𝐶𝐴𝐷 → 𝐶𝐵𝐷))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  ⟨cop 4590   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2836  df-ss 3916  df-br 5104

This theorem is used by:  ssbr  5149  sess1  5616  brrelex12  5703  eqbrrdva  5847  predtrss  6324  ersym  8723  ertr  8726  ttrclss  9714  fpwwe2lem5  10713  fpwwe2lem6  10714  fpwwe2lem8  10716  fpwwe2lem11  10719  fpwwe2lem12  10720  fpwwe2  10721  coss12d  15118  fthres2  18102  invfuc  18145  pospo  18510  dirref  18768  efgcpbl  19963  frgpuplem  19979  subrguss  20832  znleval  21853  ustref  24531  ustuqtop4  24556  metider  34519  mclsppslem  36327  fundmpss  36511  eqvrelsym  39601  eqvreltr  39603  iunrelexpuztr  44704  frege96d  44734  frege91d  44736  frege98d  44738  frege124d  44746  grucollcld  45229