Theorem sseq1 3961

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 3951	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3943	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3943	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	2, 3	anbiim 650	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
5	4	ancoms 462	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
6	1, 5	sylbi 219	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921

This theorem is referenced by:  sseq12  3963  sseq1i  3964  sseq1d  3967  nssne2  3999  psseq1  4043  uneqdifeq  4445  sbss  4473  pwjust  4555  elpwg  4557  pwpw0  4770  sssn  4783  ssunsn2  4784  unimax  4902  trss  5216  al0ssb  5257  sseliALT  5258  elssabg  5298  intabs  5304  vpwex  5333  nnullss  5428  exss  5429  releq  5747  iss  6021  relcnvtrg  6250  fununi  6592  ssimaex  6948  isofrlem  7320  onssmin  7771  tfis  7831  tfisi  7835  funcnvuni  7909  ffoss  7923  f1oweALT  7949  frxp  8101  frxp2  8119  frrlem1  8262  frrlem13  8274  tfrlem1  8341  oawordeu  8519  coflton  8636  cofon1  8637  cofon2  8638  naddunif  8659  qsss  8752  boxcutc  8919  sbthlem2  9056  sbth  9065  findcard2d  9131  ssfi  9137  sbthfi  9163  php  9171  isinf  9205  unbnn2  9237  domunfican  9262  fiint  9267  finsschain  9299  indexfi  9300  dffi3  9374  hartogslem1  9487  cantnfval2  9621  cantnfle  9623  cantnflem1  9641  tz9.1  9681  tcvalg  9688  setind  9699  frmin  9704  scott0  9841  bnd2  9848  carduni  9936  cardaleph  10042  alephinit  10048  aceq3lem  10073  dfac12lem3  10099  infmap2  10170  cflem  10198  cflemOLD  10199  cflm  10203  cflecard  10206  cfeq0  10210  cfsuc  10211  cfflb  10213  cfslb  10220  cfslb2n  10222  coftr  10227  fin23lem13  10286  fin23lem16  10289  fin23lem19  10290  fin23lem29  10295  fin1a2lem13  10366  itunitc  10375  domtriomlem  10396  axdc3lem2  10405  zorn2lem7  10456  zornn0g  10459  pwfseqlem4a  10616  pwfseqlem4  10617  wunfi  10676  wunex2  10693  wuncval  10697  rankcf  10732  tskuni  10738  axgroth6  10783  axgroth3  10786  axgroth4  10787  fzoss1  13689  fsuppmapnn0fiubex  14002  hashf1lem2  14466  cleq1lem  14992  rtrclreclem4  15071  sumeq1  15699  fsumcvg3  15739  fsum2d  15781  fsumabs  15812  fsumrlim  15822  fsumo1  15823  fsumiun  15832  prodeq1f  15919  prodeq1  15920  fprod2d  15994  lcmfunsnlem  16658  coprmprod  16678  vdwmc  16997  prmgaplem3  17072  prmgaplem4  17073  restsspw  17443  ismred2  17614  mrcval  17625  mrcuni  17636  acsfn  17674  isssc  17836  drsdirfi  18320  ipodrsima  18556  cntzssv  19351  pmtrfrn  19481  pmtrrn2  19483  pmtrdifellem1  19499  pmtrdifellem2  19500  sylow2alem2  19641  sylow2a  19642  efgval  19740  gsumzaddlem  19944  ablfac1eulem  20097  gsumle  20168  rgspnval  20641  lspval  21022  lspindpi  21182  znf1o  21583  zntoslem  21588  aspval  21904  mplsubglem  22030  mpllsslem  22031  mplcoe1  22070  mplcoe5  22073  mdetunilem9  22660  uniopn  22937  fiinopn  22941  fiinbas  22992  baspartn  22994  eltg2  22998  eltg3  23002  topbas  23012  pptbas  23048  clsval  23077  neiint  23144  neips  23153  opnneissb  23154  opnssneib  23155  innei  23165  neiptoptop  23171  neiptopnei  23172  restbas  23198  restcld  23212  neitr  23220  restcls  23221  restntr  23222  cnpdis  23333  cmpsublem  23439  cmpsub  23440  fiuncmp  23444  unconn  23469  1stcfb  23485  2ndc1stc  23491  1stcrest  23493  2ndcctbss  23495  2ndcomap  23498  dis2ndc  23500  lly1stc  23536  refssex  23551  refun0  23555  llycmpkgen2  23590  txbas  23607  eltx  23608  ptuni2  23616  neitx  23647  ptpjopn  23652  ptcld  23653  txlm  23688  tx1stc  23690  txkgen  23692  xkopt  23695  xkococnlem  23699  ptcmpfi  23853  fbssfi  23877  opnfbas  23882  isfil2  23896  isfildlem  23897  snfil  23904  fsubbas  23907  ssfg  23912  fgss2  23914  fgcl  23918  fbasrn  23924  fgtr  23930  ufli  23954  uffix  23961  rnelfmlem  23992  fclscf  24065  alexsublem  24084  alexsubALTlem2  24088  alexsubALTlem3  24089  alexsubALTlem4  24090  alexsubALT  24091  tmdgsum2  24136  subgntr  24147  opnsubg  24148  qustgpopn  24160  tsmsfbas  24168  tsmsgsum  24179  tsmsres  24184  tsmsf1o  24185  tsmsxplem1  24193  tsmsxp  24195  isust  24244  ustssel  24246  ustincl  24248  ustdiag  24249  ustinvel  24250  ustexhalf  24251  ustexsym  24256  ust0  24260  restutop  24277  ustuqtop4  24284  utopsnneiplem  24287  blssexps  24466  blssex  24467  neibl  24541  blcld  24545  met1stc  24561  met2ndci  24562  metrest  24564  prdsxmslem2  24569  metustfbas  24597  cfilucfil  24599  metuel2  24605  metustbl  24606  restmetu  24610  dscopn  24613  isngp2  24637  tgioo  24836  tgqioo  24840  zdis  24857  xrge0tsms  24875  fsumcn  24912  volivth  25649  vitalilem2  25651  itgfsum  25869  limcun  25937  recnprss  25946  dvmptfsum  26017  ftc1a  26079  plyssc  26240  efopn  26700  jensen  27030  brslts  27832  madef  27906  tglnunirn  28694  lpvtx  29215  umgredgprv  29254  usgredgprvALT  29342  issubgr2  29419  subgrprop2  29421  egrsubgr  29424  0uhgrsubgr  29426  frcond3  30417  hhsssh  31418  shintcl  31479  chintcl  31481  spanval  31482  omlsi  31553  pjoml  31585  chnlen0  31593  chsscon3  31649  chlejb1  31661  chnle  31663  spanun  31694  h1datom  31731  cmbr4i  31750  pjoml2  31760  pjoml3  31761  lecm  31766  osumcor2i  31793  osum  31794  spansncv  31802  pjcjt2  31841  pjopyth  31869  hstel2  32368  stj  32384  stcltr1i  32423  mdi  32444  mdbr3  32446  mdbr4  32447  dmdbr  32448  dmdmd  32449  dmdbr5  32457  mdsl1i  32470  mdslmd1lem3  32476  mdslmd1lem4  32477  mdslmd1i  32478  csmdsymi  32483  atss  32495  atom1d  32502  superpos  32503  chcv1  32504  shatomici  32507  shatomistici  32510  hatomistici  32511  chrelat2  32519  chirredi  32543  atcvat4i  32546  mdsymlem2  32553  mdsymlem6  32557  dmdbr6ati  32572  dmdbr7ati  32573  xrge0tsmsd  33214  gsumvsca1  33367  gsumvsca2  33368  prmidl  33587  ismxidl  33611  constrfiss  34009  zarcls1  34127  zarclsun  34128  zarclsiin  34129  zarclsint  34130  zarclssn  34131  zartop  34134  zartopon  34135  zart0  34137  zarmxt1  34138  zarcmp  34140  rhmpreimacnlem  34142  rhmpreimacn  34143  tpr2rico  34170  issiga  34370  isrnsiga  34371  sigagenval  34398  measiuns  34475  dya2icoseg  34535  dya2iocnrect  34539  dya2iocuni  34541  carsgmon  34572  carsgsigalem  34573  carsgclctunlem2  34577  carsgclctun  34579  pmeasmono  34582  pmeasadd  34583  bnj517  35144  bnj1118  35243  bnj1145  35252  bnj1154  35258  bnj1452  35311  bnj1498  35320  fineqvpow  35375  fineqvac  35376  fineqvacALT  35377  setindregs  35390  tz9.1regs  35394  fineqvr1ombregs  35398  vonf1wev  35415  vonf1owevOLD  35417  pthhashvtx  35442  kur14lem1  35520  cvmopnlem  35592  dfon2lem3  36097  dfon2lem7  36101  brsset  36201  fness  36673  fneref  36674  fnessref  36681  neibastop2lem  36684  topmeet  36688  fnejoin2  36693  tailfb  36701  filnetlem4  36705  onsucsuccmpi  36767  ttcwf2  36849  ttcexg  36856  bj-snglss  37419  bj-elpwgALT  37503  bj-restpw  37546  bj-imdirco  37646  dissneqlem  37798  relowlssretop  37821  relowlpssretop  37822  ctbssinf  37864  pibt2  37875  matunitlindflem1  38079  ptrecube  38083  poimirlem29  38112  mblfinlem2  38121  mblfinlem3  38122  mblfinlem4  38123  ismblfin  38124  ovoliunnfl  38125  voliunnfl  38127  volsupnfl  38128  indexa  38196  indexdom  38197  neificl  38216  istotbnd3  38234  sstotbnd2  38237  sstotbnd  38238  equivtotbnd  38241  ssbnd  38251  heiborlem1  38274  heiborlem6  38279  heiborlem8  38281  heiborlem10  38283  unichnidl  38494  pridl  38500  ismaxidl  38503  igenval  38524  igenval2  38529  ispridlc  38533  relcnveq3  38790  iss2  38807  brssr  39044  elrelscnveq3  39090  lsmsat  39596  lssatomic  39599  lssats  39600  lsat0cv  39621  lcvexchlem4  39625  lcvexchlem5  39626  lsatcvatlem  39637  l1cvpat  39642  ispsubsp  40333  linepsubN  40340  pclvalN  40478  ispsubclN  40525  ispsubcl2N  40535  pclfinclN  40538  diaelrnN  41633  docavalN  41711  dochval  41939  dvh4dimat  42026  dochexmidlem1  42048  lpolconN  42075  mapdordlem2  42225  eqresfnbd  42815  ismrcd1  43243  ismrcd2  43244  ismrc  43246  mzpcompact2lem  43296  aomclem6  43600  hbtlem6  43670  onintunirab  43768  rp-brsslt  43963  ssficl  44109  ssuncl  44110  ssdifcl  44111  sssymdifcl  44112  elmapintrab  44116  clcnvlem  44163  iunrelexpmin1  44248  iunrelexpmin2  44252  clsk3nimkb  44580  clsk1indlem1  44585  isotone1  44588  isotone2  44589  ntrclsiso  44607  gneispace  44674  gneispacess2  44686  onfrALTlem5  45082  onfrALTlem5VD  45424  relpfrlem  45493  modelaxreplem1  45518  islptre  46159  dvmptconst  46453  dvmptidg  46455  dvmulcncf  46463  dvdivcncf  46465  dvmptfprod  46483  stoweidlem51  46589  stoweidlem52  46590  fourierdlem103  46747  fourierdlem104  46748  ioorrnopnlem  46842  ioorrnopnxrlem  46844  salgenval  46859  ovnval2  47083  ovncvrrp  47102  ovnsubaddlem1  47108  ovnsubadd  47110  ovncvr2  47149  hspmbl  47167  elsetpreimafvssdm  47956  isubgredg  48452  uhgrimisgrgriclem  48516  grimedg  48521  grtrissvtx  48530  grtrimap  48534  stgredgiun  48544  isubgr3stgrlem6  48557  isubgr3stgrlem7  48558  uspgrlimlem1  48574  uspgrlimlem2  48575  uspgrlimlem3  48576  uspgrlimlem4  48577  clnbgrvtxedg  48580  grlimedgclnbgr  48581  grlimpredg  48584  grlimprclnbgrvtx  48585  grlimgredgex  48586  grlimgrtrilem1  48587  grlimgrtrilem2  48588  grlimgrtri  48589  usgrexmpl1lem  48607  usgrexmpl2lem  48612  uspgrsprfo  48734  unilbss  49403  sepfsepc  49513  unilbeu  49570  ipolubdm  49572  ipoglbdm  49575  discsubc  49649  iinfconstbas  49651  setrec1lem1  50272  setrec1lem4  50275  setrec2fun  50277  elsetrecslem  50284  elpglem2  50297