Theorem sseq1 3589

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 3583	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3575	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 481	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3575	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
5	4	adantr 480	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
6	3, 5	impbid 201	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
7	1, 6	sylbi 206	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  sseq12  3591  sseq1i  3592  sseq1d  3595  nssne2  3625  psseq1  3656  uneqdifeq  4009  uneqdifeqOLD  4010  sbss  4034  pwjust  4109  elpw  4114  elpwg  4116  pwpw0  4284  sssn  4298  ssunsn2  4299  pwsnALT  4367  unimax  4409  trss  4689  trssOLD  4690  sseliALT  4719  elssabg  4746  intabs  4752  nnullss  4857  exss  4858  fri  5000  releq  5124  iss  5367  relcnvtr  5572  fununi  5878  ssimaex  6173  isofrlem  6490  onssmin  6889  tfis  6946  tfisi  6950  funcnvuni  7012  ffoss  7020  f1oweALT  7043  frxp  7174  wfrlem1  7301  wfrlem4  7305  wfrlem15  7316  tfrlem1  7359  oawordeu  7522  qsss  7695  boxcutc  7837  sbthlem2  7956  sbth  7965  php  8029  isinf  8058  findcard2d  8087  unbnn2  8102  domunfican  8118  fiint  8122  finsschain  8156  indexfi  8157  dffi3  8220  hartogslem1  8330  cantnfval2  8449  cantnfle  8451  cantnflem1  8469  tz9.1  8488  setind  8493  tcvalg  8497  scott0  8632  bnd2  8639  carduni  8690  cardaleph  8795  alephinit  8801  aceq3lem  8826  dfac12lem3  8850  infmap2  8923  cflem  8951  cflm  8955  cflecard  8958  cfeq0  8961  cfsuc  8962  cfflb  8964  cfslb  8971  cfslb2n  8973  coftr  8978  fin23lem13  9037  fin23lem16  9040  fin23lem19  9041  fin23lem29  9046  fin1a2lem13  9117  itunitc  9126  domtriomlem  9147  axdc3lem2  9156  zorn2lem7  9207  zornn0g  9210  fpwwe2lem5  9335  pwfseqlem4a  9362  pwfseqlem4  9363  wunfi  9422  wunex2  9439  wuncval  9443  rankcf  9478  tskuni  9484  axgroth6  9529  axgroth3  9532  axgroth4  9533  fzoss1  12364  fsuppmapnn0fiubex  12654  hashf1lem2  13097  cleq1lem  13569  rtrclreclem4  13649  sumeq1  14267  fsumcvg3  14307  fsum2d  14344  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fsumiun  14394  prodeq1f  14477  fprod2d  14550  lcmfunsnlem  15192  coprmprod  15213  vdwmc  15520  prmgaplem3  15595  prmgaplem4  15596  restsspw  15915  ismred2  16086  mrcval  16093  mrcuni  16104  acsfn  16143  isssc  16303  drsdirfi  16761  ipodrsima  16988  cntzssv  17584  pmtrfrn  17701  pmtrrn2  17703  pmtrdifellem1  17719  pmtrdifellem2  17720  isslw  17846  sylow2alem2  17856  sylow2a  17857  efgval  17953  gsumzaddlem  18144  ablfac1eulem  18294  lspval  18796  lspindpi  18953  aspval  19149  mplsubglem  19255  mpllsslem  19256  mplcoe1  19286  mplcoe5  19289  znf1o  19719  zntoslem  19724  mdetunilem9  20245  uniopn  20527  fiinopn  20531  fiinbas  20567  baspartn  20569  eltg2  20573  eltg3  20577  topbas  20587  pptbas  20622  clsval  20651  neival  20716  neiint  20718  neips  20727  opnneissb  20728  opnssneib  20729  innei  20739  neiptoptop  20745  neiptopnei  20746  restbas  20772  restcld  20786  neitr  20794  restcls  20795  restntr  20796  cnpdis  20907  nrmsep3  20969  cmpsublem  21012  cmpsub  21013  fiuncmp  21017  uncon  21042  1stcfb  21058  2ndc1stc  21064  1stcrest  21066  2ndcctbss  21068  2ndcomap  21071  dis2ndc  21073  lly1stc  21109  refssex  21124  refun0  21128  llycmpkgen2  21163  txbas  21180  eltx  21181  ptuni2  21189  neitx  21220  ptpjopn  21225  ptcld  21226  txlm  21261  tx1stc  21263  txkgen  21265  xkopt  21268  xkococnlem  21272  ptcmpfi  21426  fbssfi  21451  opnfbas  21456  isfil2  21470  isfildlem  21471  snfil  21478  fsubbas  21481  ssfg  21486  fgss2  21488  fgcl  21492  fbasrn  21498  fgtr  21504  ufli  21528  uffix  21535  rnelfmlem  21566  fclscf  21639  alexsublem  21658  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  tmdgsum2  21710  subgntr  21720  opnsubg  21721  qustgpopn  21733  tsmsfbas  21741  tsmsgsum  21752  tsmsres  21757  tsmsf1o  21758  tsmsxplem1  21766  tsmsxp  21768  isust  21817  ustssel  21819  ustincl  21821  ustdiag  21822  ustinvel  21823  ustexhalf  21824  ustexsym  21829  ust0  21833  restutop  21851  ustuqtop4  21858  utopsnneiplem  21861  blssexps  22041  blssex  22042  neibl  22116  blcld  22120  met1stc  22136  met2ndci  22137  metrest  22139  prdsxmslem2  22144  metustfbas  22172  cfilucfil  22174  metuel2  22180  metustbl  22181  restmetu  22185  dscopn  22188  isngp2  22211  tgioo  22407  tgqioo  22411  zdis  22427  xrge0tsms  22445  fsumcn  22481  ovolval  23049  volivth  23181  vitalilem2  23184  itgfsum  23399  limcun  23465  recnprss  23474  dvmptfsum  23542  ftc1a  23604  plyssc  23760  efopn  24204  jensen  24515  tglnunirn  25243  lpvtx  25734  umgredgprv  25773  usgraedgprv  25905  frisusgranb  26524  hhsssh  27510  shintcl  27573  chintcl  27575  spanval  27576  omlsi  27647  pjoml  27679  chnlen0  27687  chsscon3  27743  chlejb1  27755  chnle  27757  spanun  27788  h1datom  27825  cmbr4i  27844  pjoml2  27854  pjoml3  27855  lecm  27860  osumcor2i  27887  osum  27888  spansncv  27896  pjcjt2  27935  pjopyth  27963  hstel2  28462  stj  28478  stcltr1i  28517  mdi  28538  mdbr3  28540  mdbr4  28541  dmdbr  28542  dmdmd  28543  dmdbr5  28551  mdsl1i  28564  mdslmd1lem3  28570  mdslmd1lem4  28571  mdslmd1i  28572  csmdsymi  28577  atss  28589  atom1d  28596  superpos  28597  chcv1  28598  shatomici  28601  shatomistici  28604  hatomistici  28605  chrelat2  28613  chirredi  28637  atcvat4i  28640  mdsymlem2  28647  mdsymlem6  28651  dmdbr6ati  28666  dmdbr7ati  28667  gsumle  29110  gsumvsca1  29113  gsumvsca2  29114  xrge0tsmsd  29116  tpr2rico  29286  issiga  29501  isrnsigaOLD  29502  isrnsiga  29503  sigagenval  29530  measiuns  29607  dya2icoseg  29666  dya2iocnrect  29670  dya2iocuni  29672  carsgmon  29703  carsgsigalem  29704  carsgclctunlem2  29708  carsgclctun  29710  pmeasmono  29713  pmeasadd  29714  bnj517  30209  bnj1118  30306  bnj1145  30315  bnj1154  30321  bnj1452  30374  bnj1498  30383  kur14lem1  30442  cvmopnlem  30514  dfon2lem3  30934  dfon2lem7  30938  frmin  30983  frrlem1  31024  frrlem3  31026  brsset  31166  fness  31514  fneref  31515  fnessref  31522  neibastop2lem  31525  topmeet  31529  fnejoin2  31534  tailfb  31542  filnetlem4  31546  onsucsuccmpi  31612  bj-snglss  32151  bj-restpw  32226  dissneqlem  32363  relowlssretop  32387  relowlpssretop  32388  matunitlindflem1  32575  ptrecube  32579  poimirlem29  32608  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  indexa  32698  indexdom  32699  neificl  32719  istotbnd3  32740  sstotbnd2  32743  sstotbnd  32744  equivtotbnd  32747  ssbnd  32757  heiborlem1  32780  heiborlem6  32785  heiborlem8  32787  heiborlem10  32789  unichnidl  33000  pridl  33006  ismaxidl  33009  igenval  33030  igenval2  33035  ispridlc  33039  lsmsat  33313  lssatomic  33316  lssats  33317  lsat0cv  33338  lcvexchlem4  33342  lcvexchlem5  33343  lsatcvatlem  33354  l1cvpat  33359  ispsubsp  34049  linepsubN  34056  pclvalN  34194  ispsubclN  34241  ispsubcl2N  34251  pclfinclN  34254  diaelrnN  35352  docavalN  35430  dochval  35658  dvh4dimat  35745  dochexmidlem1  35767  lpolconN  35794  mapdordlem2  35944  ismrcd1  36279  ismrcd2  36280  ismrc  36282  mzpcompact2lem  36332  aomclem6  36647  hbtlem6  36718  rgspnval  36757  ssficl  36893  ssuncl  36894  ssdifcl  36895  sssymdifcl  36896  elmapintrab  36901  clcnvlem  36949  iunrelexpmin1  37019  iunrelexpmin2  37023  clsk3nimkb  37358  clsk1indlem1  37363  isotone1  37366  isotone2  37367  ntrclsiso  37385  gneispace  37452  gneispacess2  37464  onfrALTlem5  37778  onfrALTlem5VD  38143  islptre  38686  dvmptconst  38803  dvmptidg  38805  dvmulcncf  38815  dvdivcncf  38817  dvmptfprod  38835  stoweidlem51  38944  stoweidlem52  38945  fourierdlem103  39102  fourierdlem104  39103  ioorrnopnlem  39200  ioorrnopnxrlem  39202  salgenval  39217  ovnval2  39435  ovncvrrp  39454  ovnsubaddlem1  39460  ovnsubadd  39462  ovncvr2  39501  hspmbl  39519  usgredgprvALT  40422  issubgr2  40496  subgrprop2  40498  egrsubgr  40501  0uhgrsubgr  40503  frcond3  41440  setrec1lem1  42233  setrec1lem4  42236  setrec2fun  42238  elsetrecslem  42243  elpglem2  42254