Theorem sseq1 3942

Description: Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Assertion

Ref	Expression
sseq1	⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Proof of Theorem sseq1

Step	Hyp	Ref	Expression
1		eqss 3932	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3924	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 481	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3924	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
5	4	adantr 480	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
6	3, 5	impbid 211	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
7	1, 6	sylbi 216	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sseq12  3944  sseq1i  3945  sseq1d  3948  nssne2  3978  psseq1  4018  uneqdifeq  4420  sbss  4450  pwjust  4531  elpwg  4533  elpwOLD  4536  elpwgOLD  4537  pwpw0  4743  sssn  4756  ssunsn2  4757  pwsnOLD  4829  unimax  4874  trss  5196  al0ssb  5227  sseliALT  5228  elssabg  5255  intabs  5261  vpwex  5295  nnullss  5371  exss  5372  friOLD  5541  releq  5677  iss  5932  relcnvtrg  6159  fununi  6493  ssimaex  6835  isofrlem  7191  onssmin  7619  tfis  7676  tfisi  7680  funcnvuni  7752  ffoss  7762  f1oweALT  7788  frxp  7938  frrlem1  8073  frrlem13  8085  wfrlem1OLD  8110  wfrlem4OLD  8114  wfrlem15OLD  8125  tfrlem1  8178  oawordeu  8348  qsss  8525  boxcutc  8687  sbthlem2  8824  sbth  8833  php  8897  findcard2d  8911  ssfi  8918  sbthfi  8942  isinf  8965  unbnn2  9001  domunfican  9017  fiint  9021  finsschain  9056  indexfi  9057  dffi3  9120  hartogslem1  9231  cantnfval2  9357  cantnfle  9359  cantnflem1  9377  tz9.1  9418  setind  9423  tcvalg  9427  frmin  9438  scott0  9575  bnd2  9582  carduni  9670  cardaleph  9776  alephinit  9782  aceq3lem  9807  dfac12lem3  9832  infmap2  9905  cflem  9933  cflm  9937  cflecard  9940  cfeq0  9943  cfsuc  9944  cfflb  9946  cfslb  9953  cfslb2n  9955  coftr  9960  fin23lem13  10019  fin23lem16  10022  fin23lem19  10023  fin23lem29  10028  fin1a2lem13  10099  itunitc  10108  domtriomlem  10129  axdc3lem2  10138  zorn2lem7  10189  zornn0g  10192  fpwwe2lem4  10321  pwfseqlem4a  10348  pwfseqlem4  10349  wunfi  10408  wunex2  10425  wuncval  10429  rankcf  10464  tskuni  10470  axgroth6  10515  axgroth3  10518  axgroth4  10519  fzoss1  13342  fsuppmapnn0fiubex  13640  hashf1lem2  14098  cleq1lem  14621  rtrclreclem4  14700  sumeq1  15328  fsumcvg3  15369  fsum2d  15411  fsumabs  15441  fsumrlim  15451  fsumo1  15452  fsumiun  15461  prodeq1f  15546  fprod2d  15619  lcmfunsnlem  16274  coprmprod  16294  vdwmc  16607  prmgaplem3  16682  prmgaplem4  16683  restsspw  17059  ismred2  17229  mrcval  17236  mrcuni  17247  acsfn  17285  isssc  17449  drsdirfi  17938  ipodrsima  18174  cntzssv  18849  pmtrfrn  18981  pmtrrn2  18983  pmtrdifellem1  18999  pmtrdifellem2  19000  sylow2alem2  19138  sylow2a  19139  efgval  19238  gsumzaddlem  19437  ablfac1eulem  19590  lspval  20152  lspindpi  20309  znf1o  20671  zntoslem  20676  aspval  20987  mplsubglem  21115  mpllsslem  21116  mplcoe1  21148  mplcoe5  21151  mdetunilem9  21677  uniopn  21954  fiinopn  21958  fiinbas  22010  baspartn  22012  eltg2  22016  eltg3  22020  topbas  22030  pptbas  22066  clsval  22096  neiint  22163  neips  22172  opnneissb  22173  opnssneib  22174  innei  22184  neiptoptop  22190  neiptopnei  22191  restbas  22217  restcld  22231  neitr  22239  restcls  22240  restntr  22241  cnpdis  22352  cmpsublem  22458  cmpsub  22459  fiuncmp  22463  unconn  22488  1stcfb  22504  2ndc1stc  22510  1stcrest  22512  2ndcctbss  22514  2ndcomap  22517  dis2ndc  22519  lly1stc  22555  refssex  22570  refun0  22574  llycmpkgen2  22609  txbas  22626  eltx  22627  ptuni2  22635  neitx  22666  ptpjopn  22671  ptcld  22672  txlm  22707  tx1stc  22709  txkgen  22711  xkopt  22714  xkococnlem  22718  ptcmpfi  22872  fbssfi  22896  opnfbas  22901  isfil2  22915  isfildlem  22916  snfil  22923  fsubbas  22926  ssfg  22931  fgss2  22933  fgcl  22937  fbasrn  22943  fgtr  22949  ufli  22973  uffix  22980  rnelfmlem  23011  fclscf  23084  alexsublem  23103  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  alexsubALT  23110  tmdgsum2  23155  subgntr  23166  opnsubg  23167  qustgpopn  23179  tsmsfbas  23187  tsmsgsum  23198  tsmsres  23203  tsmsf1o  23204  tsmsxplem1  23212  tsmsxp  23214  isust  23263  ustssel  23265  ustincl  23267  ustdiag  23268  ustinvel  23269  ustexhalf  23270  ustexsym  23275  ust0  23279  restutop  23297  ustuqtop4  23304  utopsnneiplem  23307  blssexps  23487  blssex  23488  neibl  23563  blcld  23567  met1stc  23583  met2ndci  23584  metrest  23586  prdsxmslem2  23591  metustfbas  23619  cfilucfil  23621  metuel2  23627  metustbl  23628  restmetu  23632  dscopn  23635  isngp2  23659  tgioo  23865  tgqioo  23869  zdis  23885  xrge0tsms  23903  fsumcn  23939  volivth  24676  vitalilem2  24678  itgfsum  24896  limcun  24964  recnprss  24973  dvmptfsum  25044  ftc1a  25106  plyssc  25266  efopn  25718  jensen  26043  tglnunirn  26813  lpvtx  27341  umgredgprv  27380  usgredgprvALT  27465  issubgr2  27542  subgrprop2  27544  egrsubgr  27547  0uhgrsubgr  27549  frcond3  28534  hhsssh  29532  shintcl  29593  chintcl  29595  spanval  29596  omlsi  29667  pjoml  29699  chnlen0  29707  chsscon3  29763  chlejb1  29775  chnle  29777  spanun  29808  h1datom  29845  cmbr4i  29864  pjoml2  29874  pjoml3  29875  lecm  29880  osumcor2i  29907  osum  29908  spansncv  29916  pjcjt2  29955  pjopyth  29983  hstel2  30482  stj  30498  stcltr1i  30537  mdi  30558  mdbr3  30560  mdbr4  30561  dmdbr  30562  dmdmd  30563  dmdbr5  30571  mdsl1i  30584  mdslmd1lem3  30590  mdslmd1lem4  30591  mdslmd1i  30592  csmdsymi  30597  atss  30609  atom1d  30616  superpos  30617  chcv1  30618  shatomici  30621  shatomistici  30624  hatomistici  30625  chrelat2  30633  chirredi  30657  atcvat4i  30660  mdsymlem2  30667  mdsymlem6  30671  dmdbr6ati  30686  dmdbr7ati  30687  xrge0tsmsd  31219  gsumle  31252  gsumvsca1  31381  gsumvsca2  31382  prmidl  31517  ismxidl  31536  zarcls1  31721  zarclsun  31722  zarclsiin  31723  zarclsint  31724  zarclssn  31725  zartop  31728  zartopon  31729  zart0  31731  zarmxt1  31732  zarcmp  31734  rhmpreimacnlem  31736  rhmpreimacn  31737  tpr2rico  31764  issiga  31980  isrnsiga  31981  sigagenval  32008  measiuns  32085  dya2icoseg  32144  dya2iocnrect  32148  dya2iocuni  32150  carsgmon  32181  carsgsigalem  32182  carsgclctunlem2  32186  carsgclctun  32188  pmeasmono  32191  pmeasadd  32192  bnj517  32765  bnj1118  32864  bnj1145  32873  bnj1154  32879  bnj1452  32932  bnj1498  32941  fineqvpow  32965  fineqvac  32966  fineqvacALT  32967  pthhashvtx  32989  kur14lem1  33068  cvmopnlem  33140  dfon2lem3  33667  dfon2lem7  33671  frxp2  33718  frxp3  33724  brsslt  33907  madef  33967  brsset  34118  fness  34465  fneref  34466  fnessref  34473  neibastop2lem  34476  topmeet  34480  fnejoin2  34485  tailfb  34493  filnetlem4  34497  onsucsuccmpi  34559  bj-snglss  35087  bj-restpw  35190  bj-imdirco  35288  dissneqlem  35438  relowlssretop  35461  relowlpssretop  35462  ctbssinf  35504  pibt2  35515  matunitlindflem1  35700  ptrecube  35704  poimirlem29  35733  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  indexa  35818  indexdom  35819  neificl  35838  istotbnd3  35856  sstotbnd2  35859  sstotbnd  35860  equivtotbnd  35863  ssbnd  35873  heiborlem1  35896  heiborlem6  35901  heiborlem8  35903  heiborlem10  35905  unichnidl  36116  pridl  36122  ismaxidl  36125  igenval  36146  igenval2  36151  ispridlc  36155  relcnveq3  36383  iss2  36406  elrelscnveq3  36536  brssr  36546  lsmsat  36949  lssatomic  36952  lssats  36953  lsat0cv  36974  lcvexchlem4  36978  lcvexchlem5  36979  lsatcvatlem  36990  l1cvpat  36995  ispsubsp  37686  linepsubN  37693  pclvalN  37831  ispsubclN  37878  ispsubcl2N  37888  pclfinclN  37891  diaelrnN  38986  docavalN  39064  dochval  39292  dvh4dimat  39379  dochexmidlem1  39401  lpolconN  39428  mapdordlem2  39578  ismrcd1  40436  ismrcd2  40437  ismrc  40439  mzpcompact2lem  40489  aomclem6  40800  hbtlem6  40870  rgspnval  40909  ssficl  41065  ssuncl  41066  ssdifcl  41067  sssymdifcl  41068  elmapintrab  41073  clcnvlem  41120  iunrelexpmin1  41205  iunrelexpmin2  41209  clsk3nimkb  41539  clsk1indlem1  41544  isotone1  41547  isotone2  41548  ntrclsiso  41566  gneispace  41633  gneispacess2  41645  onfrALTlem5  42051  onfrALTlem5VD  42394  islptre  43050  dvmptconst  43346  dvmptidg  43348  dvmulcncf  43356  dvdivcncf  43358  dvmptfprod  43376  stoweidlem51  43482  stoweidlem52  43483  fourierdlem103  43640  fourierdlem104  43641  ioorrnopnlem  43735  ioorrnopnxrlem  43737  salgenval  43752  ovnval2  43973  ovncvrrp  43992  ovnsubaddlem1  43998  ovnsubadd  44000  ovncvr2  44039  hspmbl  44057  elsetpreimafvssdm  44726  uspgrsprfo  45198  unilbss  46051  sepfsepc  46109  unilbeu  46159  ipolubdm  46161  ipoglbdm  46164  setrec1lem1  46279  setrec1lem4  46282  setrec2fun  46284  elsetrecslem  46290  elpglem2  46303