Theorem ssbrd 5154

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900  ⟨cop 4840   class class class wbr 5108

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 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839  df-ss 3901  df-br 5109

This theorem is used by:  ssbr  5155  sess1  5623  brrelex12  5710  eqbrrdva  5859  predtrss  6351  ersym  8768  ertr  8771  ttrclss  9758  fpwwe2lem5  10759  fpwwe2lem6  10760  fpwwe2lem8  10762  fpwwe2lem11  10765  fpwwe2lem12  10766  fpwwe2  10767  coss12dOLD  15168  fthres2  18159  invfuc  18202  pospo  18567  dirref  18825  efgcpbl  20021  frgpuplem  20037  subrguss  20890  znleval  21915  ustref  24593  ustuqtop4  24618  metider  34637  mclsppslem  36556  fundmpss  36747  eqvrelsym  39887  eqvreltr  39889  iunrelexpuztr  44980  frege96d  45010  frege91d  45012  frege98d  45014  frege124d  45022  grucollcld  45505