Theorem sseqtrd 3974

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

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

Assertion

Ref	Expression
sseqtrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrd

Step	Hyp	Ref	Expression
1		sseqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	sseq2d 3970	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶))
4	1, 3	mpbid 232	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  sseqtrrd  3975  sseqtrid  3980  3sstr3d  3992  uniintsn  4938  fssdmd  6674  oeeui  8527  nnaword2  8555  oaabs2  8574  naddword2  8617  erssxp  8655  fipwuni  9335  cantnflem3  9606  ficardun2  10115  ackbij1lem12  10143  ackbij1b  10151  fin1a2lem13  10325  winafp  10610  ioodisj  13403  reltrclfv  14942  prodss  15872  mrcssv  17538  mrcsscl  17544  mrcuni  17545  mressmrcd  17551  mreexexlem2d  17569  mreexexlem3d  17570  mreexfidimd  17574  subcss2  17768  resssetc  18017  funcsetcres2  18018  estrres  18063  poslubdg  18336  ipodrsfi  18463  acsmap2d  18479  mrelatlub  18486  mreclatBAD  18487  subsubmgm  18602  subsubm  18708  subsubg  19046  trivsubgd  19050  trivnsgd  19069  oppglsm  19539  subglsm  19570  lsmdisj  19578  gsumval3  19804  dprdres  19927  dprdss  19928  dprd2da  19941  dmdprdsplit2lem  19944  ablfac1b  19969  pgpfac1lem3  19976  subsubrng  20466  subsubrg  20501  rgspnval  20515  issubdrg  20683  islssd  20856  lspun  20908  lspssp  20909  lsslsp  20936  lsslspOLD  20937  lsmssspx  21010  lspabs2  21045  lspabs3  21046  lspsolvlem  21067  lbsextlem3  21085  qsssubdrg  21351  obselocv  21653  lsslindf  21755  sraassa  21794  mplbas2  21965  gsumply1subr  22134  tgcl  22872  basgen  22891  tgfiss  22894  bastop1  22896  bastop2  22897  clsss2  22975  elcls3  22986  topssnei  23027  neiptopnei  23035  neitr  23083  restcls  23084  restlp  23086  ordtrest2  23107  iscncl  23172  cncls2  23176  cncls  23177  cnntr  23178  lmcls  23205  tgcmp  23304  cmpcld  23305  uncmp  23306  hauscmplem  23309  cmpfi  23311  clsconn  23333  2ndcsb  23352  2ndcctbss  23358  2ndcomap  23361  nllyrest  23389  1stckgenlem  23456  kgencn2  23460  kgen2cn  23462  ptbasfi  23484  txcld  23506  txcls  23507  txbasval  23509  neitx  23510  ptcld  23516  ptclsg  23518  txnlly  23540  hausdiag  23548  txkgen  23555  xkopt  23558  xkopjcn  23559  xkococnlem  23562  cnmpt1res  23579  cnmpt2res  23580  imasnopn  23593  imasncld  23594  imasncls  23595  qtopcld  23616  qtoprest  23620  qtopcmap  23622  kqcldsat  23636  kqreglem2  23645  kqnrmlem2  23647  hmeontr  23672  neifil  23783  fgtr  23793  trnei  23795  uffixfr  23826  uffix2  23827  uffixsn  23828  elflim  23874  flimclslem  23887  fclsopn  23917  fclscmpi  23932  fclscmp  23933  alexsubALTlem3  23952  alexsubALT  23954  ptcmplem3  23957  subgntr  24010  opnsubg  24011  clssubg  24012  clsnsg  24013  cldsubg  24014  tgpconncompeqg  24015  snclseqg  24019  tsmsgsum  24042  tsmsid  24043  tgptsmscld  24054  ustssco  24118  utop2nei  24154  utop3cls  24155  utopreg  24156  cnextucn  24206  ressprdsds  24275  lpbl  24407  met2ndci  24426  prdsxmslem2  24433  metustexhalf  24460  psmetutop  24471  tgioo  24700  metdstri  24756  metdseq0  24759  xlebnum  24880  clsocv  25166  metelcls  25221  metsscmetcld  25231  cmetss  25232  relcmpcmet  25234  cmpcmet  25235  minveclem4a  25346  uniioovol  25496  uniioombllem3  25502  limcres  25803  dvbss  25818  perfdvf  25820  dvreslem  25826  dvres2lem  25827  dvmptresicc  25833  dvcnp2  25837  dvcnp2OLD  25838  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvcmulf  25864  dvcj  25870  dvnfre  25872  dvmptres2  25882  dvmptcmul  25884  dvmptntr  25891  dvlip2  25916  dvcnvrelem2  25939  ftc1cn  25966  dvntaylp  26295  taylthlem1  26297  ulmdvlem3  26327  pserulm  26347  nodense  27620  mulsproplem13  28054  mulsproplem14  28055  shsub2  31287  spanssoc  31311  shub2  31345  ococin  31370  ssjo  31409  chub2  31470  spanpr  31542  elnlfn  31890  mdslj1i  32281  mdslmd3i  32294  mdexchi  32297  chirredlem1  32352  atcvat3i  32358  mdsymlem1  32365  mdsymlem5  32369  imadifxp  32563  fnpreimac  32628  suppovss  32637  symgcom2  33039  pmtrcnelor  33046  cycpmco2f1  33079  0ringsubrg  33204  erlval  33211  1fldgenq  33274  0ringidl  33371  elrspunidl  33378  0ringprmidl  33399  drngmxidl  33427  drngmxidlr  33428  idlsrgmulrss1  33461  idlsrgmulrss2  33462  1arithidomlem2  33486  ply1dg3rt0irred  33530  resssra  33562  lsssra  33563  drgextlsp  33568  lvecdim0  33581  lbslsat  33591  dimkerim  33602  fedgmullem2  33605  fedgmul  33606  fldgenfldext  33642  fldextrspunlsplem  33647  fldextrspunlsp  33648  fldextrspunlem1  33649  fldextrspunfld  33650  fldextrspundgdvdslem  33654  fldextrspundgdvds  33655  algextdeglem3  33688  algextdeglem4  33689  qtophaus  33805  locfinreflem  33809  rspecbas  33834  zarclssn  33842  zarmxt1  33849  zarcmplem  33850  fsumcvg4  33919  esum2d  34062  omsmon  34268  omssubadd  34270  carsgclctun  34291  sitgclg  34312  eulerpartlemgf  34349  reprpmtf1o  34596  cvmscld  35248  cvmliftmolem1  35256  cvmlift2lem9  35286  cvmlift2lem11  35288  cvmlift3lem6  35299  opnregcld  36306  ivthALT  36311  neibastop2  36337  fnemeet1  36342  fnejoin1  36344  pibt2  37393  poimirlem11  37613  poimirlem12  37614  poimirlem30  37632  ftc1cnnc  37674  sstotbnd  37757  ssbnd  37770  heibor1lem  37791  heiborlem3  37795  heibor  37803  lsmsat  38989  lssats  38993  lcvexchlem3  39017  lsatcvat3  39033  lkrscss  39079  lkrpssN  39144  pmod1i  39830  pclbtwnN  39879  pclunN  39880  pclss2polN  39903  pcl0N  39904  sspmaplubN  39907  paddunN  39909  pnonsingN  39915  pclfinclN  39932  osumcllem4N  39941  dia2dimlem13  41058  dvhopellsm  41099  dvadiaN  41110  dicelval1stN  41170  dicelval2nd  41171  dihssxp  41234  dihvalrel  41261  dochsscl  41350  dihoml4  41359  dochnoncon  41373  dvh3dim3N  41431  lcfrlem2  41525  lcfrlem5  41528  lcfr  41567  lcdlsp  41603  mapdsn  41623  mapdlsm  41646  mapdpglem1  41654  mapdindp0  41701  hlhilocv  41939  primrootscoprbij  42078  rntrclfvOAI  42667  ismrcd1  42674  ismrcd2  42675  coeq0i  42729  hbtlem6  43105  iocinico  43188  omabs2  43308  naddwordnexlem4  43377  trclubNEW  43595  ntrk2imkb  44013  isotone1  44024  k0004ss3  44129  iccdifprioo  45501  limsupequzmptlem  45713  cncfuni  45871  cncfiooicclem1  45878  dvresntr  45903  itgsubsticclem  45960  fourierdlem42  46134  fourierdlem48  46139  fourierdlem49  46140  fourierdlem50  46141  qndenserrn  46284  prsal  46303  intsaluni  46314  sssalgen  46320  dfsalgen2  46326  sge0split  46394  ismeannd  46452  caragensspw  46494  caragendifcl  46499  carageniuncl  46508  caratheodorylem1  46511  hoicvrrex  46541  ovnssle  46546  ovn02  46553  ovnsubadd  46557  hoidmv1le  46579  ovnlecvr2  46595  ovncvr2  46596  isvonmbl  46623  vonmblss  46625  ovolval4lem2  46635  ovnovollem1  46641  ovnovollem2  46642  incsmf  46727  decsmf  46752  uspgropssxp  48132  mreuniss  48888  restcls2lem  48901  restcls2  48902  cnneiima  48905  imassc  49142