Theorem sseqtrrid 3956

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
sseqtrrid.1	⊢ 𝐵 ⊆ 𝐴
sseqtrrid.2	⊢ (𝜑 → 𝐶 = 𝐴)

Assertion

Ref	Expression
sseqtrrid	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Proof of Theorem sseqtrrid

Step	Hyp	Ref	Expression
1		sseqtrrid.1	. 2 ⊢ 𝐵 ⊆ 𝐴
2		sseqtrrid.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
3	2	eqcomd 2769	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	1, 3	sseqtrid 3955	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900

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-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  unissint  4935  resdif  6868  tfrlem5  8415  naddunif  8731  domss2  9183  dffi3  9450  cantnfp1lem3  9708  trcl  9756  tcid  9765  r1ordg  9812  r1sssuc  9817  ackbij1lem15  10338  cfsmolem  10375  fin1a2lem7  10511  wunex2  10850  wuncid  10855  trclfvlb  15190  rtrclreclem2  15241  fsumsplit  15936  o1fsum  16009  fprodsplit  16162  phimullem  16985  vdwlem6  17193  ressinbas  17452  mrcssid  17820  mreexexlem2d  17848  acsfiindd  18756  dirge  18806  symgbasfi  19623  efgredlemf  19985  efgredlemd  19988  gsumzres  20153  gsumzcl2  20154  gsumzf1o  20156  gsumadd  20167  gsumzsplit  20171  gsumsplit2  20173  dprd2da  20288  dmdprdsplit2lem  20291  dmdprdsplit2  20292  dmdprdsplit  20293  dprdsplit  20294  invrpropd  20678  rgspnssid  20896  srhmsubc  20962  issubdrg  21067  lspssid  21290  pjcss  22052  aspssid  22215  psdmul  22517  istopon  23260  sscls  23404  ordtbas  23540  cncls2  23621  tgcmp  23749  cmpfi  23756  1stcfb  23793  1stckgenlem  23902  ptbasfi  23930  ptcnplem  23970  ptuncnv  24156  ptunhmeo  24157  fbasrn  24233  cnflf2  24352  fclscmp  24379  alexsublem  24393  ghmcnp  24464  tsmsgsum  24488  tsmsres  24493  tsmssplit  24501  tsmsxplem1  24502  ustssco  24564  mopnfss  24792  cnmpopc  25279  uniiccdif  25929  uniioombllem3  25936  uniioombllem4  25937  itg2splitlem  26099  itg2split  26100  itgsplit  26186  ellimc2  26227  ellimc3  26229  lhop  26366  itgpowd  26400  plyaddlem1  26562  plymullem1  26563  taylthlem2  26731  mtest  26761  xrlimcnp  27326  fsumharmonic  27369  chtdif  27515  dchrghm  27613  lgsquadlem2  27738  dchrisumlema  27845  dchrisumlem2  27847  dchrisum0lem1b  27872  dchrisum0lem1  27873  pntrlog2bndlem6  27940  pntlemf  27962  precsexlem6  28628  precsexlem7  28629  ltonold  28677  nbupgruvtxres  30018  cyclnumvtx  30418  umgr2adedgwlk  30564  umgr2adedgwlkon  30565  umgr2adedgspth  30567  ex-res  31072  spanss2  31977  mdsymi  33043  cycpmco2lem5  33761  cycpmco2lem6  33762  cycpmco2lem7  33763  cycpmco2  33764  fldgenssid  33945  vietalem  34281  ordtconnlem1  34626  issgon  34825  sssigagen  34848  measiuns  34920  sitgclg  35044  j0le  36019  cvmliftlem10  36226  satfsschain  36296  fmlasssuc  36321  satfun  36343  dfttc3gw  37489  rdgssun  38493  ftc1anclem6  38808  heibor1lem  38935  heibor  38947  divrngcl  39083  isdrngo2  39084  igenss  39188  paddunssN  41057  sspadd1  41064  sspadd2  41065  pclssidN  41144  diassdvaN  42309  dochvalr  42606  lcdvbase  42842  nacsfix  43916  isnumbasgrplem2  44298  tfsconcatrnss12  44543  trrelsuperrel2dg  44863  fvilbd  44881  relexp0a  44908  wnefimgd  45353  grumnudlem  45461  icccncfext  47102  iblsplit  47181  dirkeritg  47317  dirkercncflem2  47319  fourierdlem81  47402  fourierdlem89  47410  fourierdlem91  47412  fourierdlem92  47413  fourierdlem111  47432  fouriercn  47447  hspdifhsp  47831  3f1oss1  48350  dfnbgrss  49155  dfnbgrss2  49162  gsumsplit2f  49482  srhmsubcALTV  49627  fdivmpt  49857  fdivpm  49860  refdivpm  49861  mreclat  50316  elpglem2  51085