Theorem sseq1 4020

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  sseq12  4022  sseq1i  4023  sseq1d  4026  nssne2  4058  psseq1  4099  uneqdifeq  4498  sbss  4524  pwjust  4605  elpwg  4607  pwpw0  4817  sssn  4830  ssunsn2  4831  unimax  4948  trss  5275  al0ssb  5313  sseliALT  5314  elssabg  5348  intabs  5354  vpwex  5382  nnullss  5472  exss  5473  friOLD  5646  releq  5788  iss  6054  relcnvtrg  6287  fununi  6642  ssimaex  6993  isofrlem  7359  onssmin  7811  tfis  7875  tfisi  7879  funcnvuni  7954  ffoss  7968  f1oweALT  7995  frxp  8149  frxp2  8167  frrlem1  8309  frrlem13  8321  wfrlem1OLD  8346  wfrlem4OLD  8350  wfrlem15OLD  8361  tfrlem1  8414  oawordeu  8591  coflton  8707  cofon1  8708  cofon2  8709  naddunif  8729  qsss  8816  boxcutc  8979  sbthlem2  9122  sbth  9131  findcard2d  9204  ssfi  9211  sbthfi  9236  php  9244  phpOLD  9256  isinf  9293  isinfOLD  9294  unbnn2  9330  domunfican  9358  fiint  9363  fiintOLD  9364  finsschain  9396  indexfi  9397  dffi3  9468  hartogslem1  9579  cantnfval2  9706  cantnfle  9708  cantnflem1  9726  tz9.1  9766  setind  9771  tcvalg  9775  frmin  9786  scott0  9923  bnd2  9930  carduni  10018  cardaleph  10126  alephinit  10132  aceq3lem  10157  dfac12lem3  10183  infmap2  10254  cflem  10282  cflemOLD  10283  cflm  10287  cflecard  10290  cfeq0  10293  cfsuc  10294  cfflb  10296  cfslb  10303  cfslb2n  10305  coftr  10310  fin23lem13  10369  fin23lem16  10372  fin23lem19  10373  fin23lem29  10378  fin1a2lem13  10449  itunitc  10458  domtriomlem  10479  axdc3lem2  10488  zorn2lem7  10539  zornn0g  10542  pwfseqlem4a  10698  pwfseqlem4  10699  wunfi  10758  wunex2  10775  wuncval  10779  rankcf  10814  tskuni  10820  axgroth6  10865  axgroth3  10868  axgroth4  10869  fzoss1  13722  fsuppmapnn0fiubex  14029  hashf1lem2  14491  cleq1lem  15017  rtrclreclem4  15096  sumeq1  15721  fsumcvg3  15761  fsum2d  15803  fsumabs  15833  fsumrlim  15843  fsumo1  15844  fsumiun  15853  prodeq1f  15938  prodeq1  15939  fprod2d  16013  lcmfunsnlem  16674  coprmprod  16694  vdwmc  17011  prmgaplem3  17086  prmgaplem4  17087  restsspw  17477  ismred2  17647  mrcval  17654  mrcuni  17665  acsfn  17703  isssc  17867  drsdirfi  18362  ipodrsima  18598  cntzssv  19358  pmtrfrn  19490  pmtrrn2  19492  pmtrdifellem1  19508  pmtrdifellem2  19509  sylow2alem2  19650  sylow2a  19651  efgval  19749  gsumzaddlem  19953  ablfac1eulem  20106  rgspnval  20628  lspval  20990  lspindpi  21151  znf1o  21587  zntoslem  21592  aspval  21910  mplsubglem  22036  mpllsslem  22037  mplcoe1  22072  mplcoe5  22075  mdetunilem9  22641  uniopn  22918  fiinopn  22922  fiinbas  22974  baspartn  22976  eltg2  22980  eltg3  22984  topbas  22994  pptbas  23030  clsval  23060  neiint  23127  neips  23136  opnneissb  23137  opnssneib  23138  innei  23148  neiptoptop  23154  neiptopnei  23155  restbas  23181  restcld  23195  neitr  23203  restcls  23204  restntr  23205  cnpdis  23316  cmpsublem  23422  cmpsub  23423  fiuncmp  23427  unconn  23452  1stcfb  23468  2ndc1stc  23474  1stcrest  23476  2ndcctbss  23478  2ndcomap  23481  dis2ndc  23483  lly1stc  23519  refssex  23534  refun0  23538  llycmpkgen2  23573  txbas  23590  eltx  23591  ptuni2  23599  neitx  23630  ptpjopn  23635  ptcld  23636  txlm  23671  tx1stc  23673  txkgen  23675  xkopt  23678  xkococnlem  23682  ptcmpfi  23836  fbssfi  23860  opnfbas  23865  isfil2  23879  isfildlem  23880  snfil  23887  fsubbas  23890  ssfg  23895  fgss2  23897  fgcl  23901  fbasrn  23907  fgtr  23913  ufli  23937  uffix  23944  rnelfmlem  23975  fclscf  24048  alexsublem  24067  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  alexsubALT  24074  tmdgsum2  24119  subgntr  24130  opnsubg  24131  qustgpopn  24143  tsmsfbas  24151  tsmsgsum  24162  tsmsres  24167  tsmsf1o  24168  tsmsxplem1  24176  tsmsxp  24178  isust  24227  ustssel  24229  ustincl  24231  ustdiag  24232  ustinvel  24233  ustexhalf  24234  ustexsym  24239  ust0  24243  restutop  24261  ustuqtop4  24268  utopsnneiplem  24271  blssexps  24451  blssex  24452  neibl  24529  blcld  24533  met1stc  24549  met2ndci  24550  metrest  24552  prdsxmslem2  24557  metustfbas  24585  cfilucfil  24587  metuel2  24593  metustbl  24594  restmetu  24598  dscopn  24601  isngp2  24625  tgioo  24831  tgqioo  24835  zdis  24851  xrge0tsms  24869  fsumcn  24907  volivth  25655  vitalilem2  25657  itgfsum  25876  limcun  25944  recnprss  25953  dvmptfsum  26027  ftc1a  26092  plyssc  26253  efopn  26714  jensen  27046  brsslt  27844  madef  27909  tglnunirn  28570  lpvtx  29099  umgredgprv  29138  usgredgprvALT  29226  issubgr2  29303  subgrprop2  29305  egrsubgr  29308  0uhgrsubgr  29310  frcond3  30297  hhsssh  31297  shintcl  31358  chintcl  31360  spanval  31361  omlsi  31432  pjoml  31464  chnlen0  31472  chsscon3  31528  chlejb1  31540  chnle  31542  spanun  31573  h1datom  31610  cmbr4i  31629  pjoml2  31639  pjoml3  31640  lecm  31645  osumcor2i  31672  osum  31673  spansncv  31681  pjcjt2  31720  pjopyth  31748  hstel2  32247  stj  32263  stcltr1i  32302  mdi  32323  mdbr3  32325  mdbr4  32326  dmdbr  32327  dmdmd  32328  dmdbr5  32336  mdsl1i  32349  mdslmd1lem3  32355  mdslmd1lem4  32356  mdslmd1i  32357  csmdsymi  32362  atss  32374  atom1d  32381  superpos  32382  chcv1  32383  shatomici  32386  shatomistici  32389  hatomistici  32390  chrelat2  32398  chirredi  32422  atcvat4i  32425  mdsymlem2  32432  mdsymlem6  32436  dmdbr6ati  32451  dmdbr7ati  32452  xrge0tsmsd  33047  gsumle  33083  gsumvsca1  33214  gsumvsca2  33215  prmidl  33447  ismxidl  33469  zarcls1  33829  zarclsun  33830  zarclsiin  33831  zarclsint  33832  zarclssn  33833  zartop  33836  zartopon  33837  zart0  33839  zarmxt1  33840  zarcmp  33842  rhmpreimacnlem  33844  rhmpreimacn  33845  tpr2rico  33872  issiga  34092  isrnsiga  34093  sigagenval  34120  measiuns  34197  dya2icoseg  34258  dya2iocnrect  34262  dya2iocuni  34264  carsgmon  34295  carsgsigalem  34296  carsgclctunlem2  34300  carsgclctun  34302  pmeasmono  34305  pmeasadd  34306  bnj517  34877  bnj1118  34976  bnj1145  34985  bnj1154  34991  bnj1452  35044  bnj1498  35053  fineqvpow  35088  fineqvac  35089  fineqvacALT  35090  pthhashvtx  35111  kur14lem1  35190  cvmopnlem  35262  dfon2lem3  35766  dfon2lem7  35770  brsset  35870  fness  36331  fneref  36332  fnessref  36339  neibastop2lem  36342  topmeet  36346  fnejoin2  36351  tailfb  36359  filnetlem4  36363  onsucsuccmpi  36425  bj-snglss  36952  bj-elpwgALT  37036  bj-restpw  37074  bj-imdirco  37172  dissneqlem  37322  relowlssretop  37345  relowlpssretop  37346  ctbssinf  37388  pibt2  37399  matunitlindflem1  37602  ptrecube  37606  poimirlem29  37635  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  indexa  37719  indexdom  37720  neificl  37739  istotbnd3  37757  sstotbnd2  37760  sstotbnd  37761  equivtotbnd  37764  ssbnd  37774  heiborlem1  37797  heiborlem6  37802  heiborlem8  37804  heiborlem10  37806  unichnidl  38017  pridl  38023  ismaxidl  38026  igenval  38047  igenval2  38052  ispridlc  38056  relcnveq3  38302  iss2  38325  elrelscnveq3  38472  brssr  38482  lsmsat  38989  lssatomic  38992  lssats  38993  lsat0cv  39014  lcvexchlem4  39018  lcvexchlem5  39019  lsatcvatlem  39030  l1cvpat  39035  ispsubsp  39727  linepsubN  39734  pclvalN  39872  ispsubclN  39919  ispsubcl2N  39929  pclfinclN  39932  diaelrnN  41027  docavalN  41105  dochval  41333  dvh4dimat  41420  dochexmidlem1  41442  lpolconN  41469  mapdordlem2  41619  eqresfnbd  42251  ismrcd1  42685  ismrcd2  42686  ismrc  42688  mzpcompact2lem  42738  aomclem6  43047  hbtlem6  43117  onintunirab  43215  rp-brsslt  43412  ssficl  43558  ssuncl  43559  ssdifcl  43560  sssymdifcl  43561  elmapintrab  43565  clcnvlem  43612  iunrelexpmin1  43697  iunrelexpmin2  43701  clsk3nimkb  44029  clsk1indlem1  44034  isotone1  44037  isotone2  44038  ntrclsiso  44056  gneispace  44123  gneispacess2  44135  onfrALTlem5  44539  onfrALTlem5VD  44882  modelaxreplem1  44942  islptre  45574  dvmptconst  45870  dvmptidg  45872  dvmulcncf  45880  dvdivcncf  45882  dvmptfprod  45900  stoweidlem51  46006  stoweidlem52  46007  fourierdlem103  46164  fourierdlem104  46165  ioorrnopnlem  46259  ioorrnopnxrlem  46261  salgenval  46276  ovnval2  46500  ovncvrrp  46519  ovnsubaddlem1  46525  ovnsubadd  46527  ovncvr2  46566  hspmbl  46584  elsetpreimafvssdm  47310  isubgredg  47789  uhgrimisgrgriclem  47835  grimedg  47840  grtrissvtx  47848  grtrimap  47850  stgredgiun  47860  isubgr3stgrlem6  47873  isubgr3stgrlem7  47874  uspgrlimlem1  47890  uspgrlimlem2  47891  uspgrlimlem3  47892  uspgrlimlem4  47893  grlimgrtrilem1  47896  grlimgrtrilem2  47897  grlimgrtri  47898  usgrexmpl1lem  47915  usgrexmpl2lem  47920  uspgrsprfo  47991  unilbss  48665  sepfsepc  48723  unilbeu  48773  ipolubdm  48775  ipoglbdm  48778  setrec1lem1  48917  setrec1lem4  48920  setrec2fun  48922  elsetrecslem  48929  elpglem2  48942