Theorem sseq1 3947

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 3937	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3929	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3929	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	2, 3	anbiim 647	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
5	4	ancoms 459	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
6	1, 5	sylbi 218	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  sseq12  3949  sseq1i  3950  sseq1d  3953  nssne2  3985  psseq1  4028  uneqdifeq  4427  sbss  4455  pwjust  4537  elpwg  4539  pwpw0  4751  sssn  4764  ssunsn2  4765  unimax  4882  trss  5196  al0ssb  5237  sseliALT  5238  elssabg  5278  intabs  5284  vpwex  5313  nnullss  5408  exss  5409  releq  5727  iss  5994  relcnvtrg  6225  fununi  6567  ssimaex  6919  isofrlem  7291  onssmin  7742  tfis  7802  tfisi  7806  funcnvuni  7879  ffoss  7895  f1oweALT  7921  frxp  8073  frxp2  8091  frrlem1  8233  frrlem13  8245  tfrlem1  8312  oawordeu  8487  coflton  8604  cofon1  8605  cofon2  8606  naddunif  8626  qsss  8719  boxcutc  8886  sbthlem2  9023  sbth  9032  findcard2d  9098  ssfi  9104  sbthfi  9130  php  9138  isinf  9172  unbnn2  9204  domunfican  9229  fiint  9234  finsschain  9266  indexfi  9267  dffi3  9341  hartogslem1  9454  cantnfval2  9588  cantnfle  9590  cantnflem1  9608  tz9.1  9648  tcvalg  9655  setind  9666  frmin  9671  scott0  9808  bnd2  9815  carduni  9903  cardaleph  10009  alephinit  10015  aceq3lem  10040  dfac12lem3  10066  infmap2  10137  cflem  10165  cflemOLD  10166  cflm  10170  cflecard  10173  cfeq0  10176  cfsuc  10177  cfflb  10179  cfslb  10186  cfslb2n  10188  coftr  10193  fin23lem13  10252  fin23lem16  10255  fin23lem19  10256  fin23lem29  10261  fin1a2lem13  10332  itunitc  10341  domtriomlem  10362  axdc3lem2  10371  zorn2lem7  10422  zornn0g  10425  pwfseqlem4a  10582  pwfseqlem4  10583  wunfi  10642  wunex2  10659  wuncval  10663  rankcf  10698  tskuni  10704  axgroth6  10749  axgroth3  10752  axgroth4  10753  fzoss1  13639  fsuppmapnn0fiubex  13952  hashf1lem2  14416  cleq1lem  14942  rtrclreclem4  15021  sumeq1  15649  fsumcvg3  15689  fsum2d  15731  fsumabs  15762  fsumrlim  15772  fsumo1  15773  fsumiun  15782  prodeq1f  15869  prodeq1  15870  fprod2d  15944  lcmfunsnlem  16608  coprmprod  16628  vdwmc  16947  prmgaplem3  17022  prmgaplem4  17023  restsspw  17392  ismred2  17563  mrcval  17574  mrcuni  17585  acsfn  17623  isssc  17785  drsdirfi  18269  ipodrsima  18505  cntzssv  19301  pmtrfrn  19431  pmtrrn2  19433  pmtrdifellem1  19449  pmtrdifellem2  19450  sylow2alem2  19591  sylow2a  19592  efgval  19690  gsumzaddlem  19894  ablfac1eulem  20047  gsumle  20118  rgspnval  20591  lspval  20972  lspindpi  21132  znf1o  21533  zntoslem  21538  aspval  21854  mplsubglem  21980  mpllsslem  21981  mplcoe1  22020  mplcoe5  22023  mdetunilem9  22610  uniopn  22887  fiinopn  22891  fiinbas  22942  baspartn  22944  eltg2  22948  eltg3  22952  topbas  22962  pptbas  22998  clsval  23027  neiint  23094  neips  23103  opnneissb  23104  opnssneib  23105  innei  23115  neiptoptop  23121  neiptopnei  23122  restbas  23148  restcld  23162  neitr  23170  restcls  23171  restntr  23172  cnpdis  23283  cmpsublem  23389  cmpsub  23390  fiuncmp  23394  unconn  23419  1stcfb  23435  2ndc1stc  23441  1stcrest  23443  2ndcctbss  23445  2ndcomap  23448  dis2ndc  23450  lly1stc  23486  refssex  23501  refun0  23505  llycmpkgen2  23540  txbas  23557  eltx  23558  ptuni2  23566  neitx  23597  ptpjopn  23602  ptcld  23603  txlm  23638  tx1stc  23640  txkgen  23642  xkopt  23645  xkococnlem  23649  ptcmpfi  23803  fbssfi  23827  opnfbas  23832  isfil2  23846  isfildlem  23847  snfil  23854  fsubbas  23857  ssfg  23862  fgss2  23864  fgcl  23868  fbasrn  23874  fgtr  23880  ufli  23904  uffix  23911  rnelfmlem  23942  fclscf  24015  alexsublem  24034  alexsubALTlem2  24038  alexsubALTlem3  24039  alexsubALTlem4  24040  alexsubALT  24041  tmdgsum2  24086  subgntr  24097  opnsubg  24098  qustgpopn  24110  tsmsfbas  24118  tsmsgsum  24129  tsmsres  24134  tsmsf1o  24135  tsmsxplem1  24143  tsmsxp  24145  isust  24194  ustssel  24196  ustincl  24198  ustdiag  24199  ustinvel  24200  ustexhalf  24201  ustexsym  24206  ust0  24210  restutop  24227  ustuqtop4  24234  utopsnneiplem  24237  blssexps  24416  blssex  24417  neibl  24491  blcld  24495  met1stc  24511  met2ndci  24512  metrest  24514  prdsxmslem2  24519  metustfbas  24547  cfilucfil  24549  metuel2  24555  metustbl  24556  restmetu  24560  dscopn  24563  isngp2  24587  tgioo  24786  tgqioo  24790  zdis  24807  xrge0tsms  24825  fsumcn  24862  volivth  25599  vitalilem2  25601  itgfsum  25819  limcun  25887  recnprss  25896  dvmptfsum  25967  ftc1a  26029  plyssc  26190  efopn  26647  jensen  26977  brslts  27779  madef  27853  tglnunirn  28641  lpvtx  29162  umgredgprv  29201  usgredgprvALT  29289  issubgr2  29366  subgrprop2  29368  egrsubgr  29371  0uhgrsubgr  29373  frcond3  30364  hhsssh  31365  shintcl  31426  chintcl  31428  spanval  31429  omlsi  31500  pjoml  31532  chnlen0  31540  chsscon3  31596  chlejb1  31608  chnle  31610  spanun  31641  h1datom  31678  cmbr4i  31697  pjoml2  31707  pjoml3  31708  lecm  31713  osumcor2i  31740  osum  31741  spansncv  31749  pjcjt2  31788  pjopyth  31816  hstel2  32315  stj  32331  stcltr1i  32370  mdi  32391  mdbr3  32393  mdbr4  32394  dmdbr  32395  dmdmd  32396  dmdbr5  32404  mdsl1i  32417  mdslmd1lem3  32423  mdslmd1lem4  32424  mdslmd1i  32425  csmdsymi  32430  atss  32442  atom1d  32449  superpos  32450  chcv1  32451  shatomici  32454  shatomistici  32457  hatomistici  32458  chrelat2  32466  chirredi  32490  atcvat4i  32493  mdsymlem2  32500  mdsymlem6  32504  dmdbr6ati  32519  dmdbr7ati  32520  xrge0tsmsd  33161  gsumvsca1  33314  gsumvsca2  33315  prmidl  33530  ismxidl  33552  constrfiss  33942  zarcls1  34060  zarclsun  34061  zarclsiin  34062  zarclsint  34063  zarclssn  34064  zartop  34067  zartopon  34068  zart0  34070  zarmxt1  34071  zarcmp  34073  rhmpreimacnlem  34075  rhmpreimacn  34076  tpr2rico  34103  issiga  34303  isrnsiga  34304  sigagenval  34331  measiuns  34408  dya2icoseg  34468  dya2iocnrect  34472  dya2iocuni  34474  carsgmon  34505  carsgsigalem  34506  carsgclctunlem2  34510  carsgclctun  34512  pmeasmono  34515  pmeasadd  34516  bnj517  35074  bnj1118  35173  bnj1145  35182  bnj1154  35188  bnj1452  35241  bnj1498  35250  fineqvpow  35303  fineqvac  35304  fineqvacALT  35305  setindregs  35318  tz9.1regs  35322  fineqvr1ombregs  35326  vonf1owev  35343  pthhashvtx  35363  kur14lem1  35441  cvmopnlem  35513  dfon2lem3  36018  dfon2lem7  36022  brsset  36122  fness  36584  fneref  36585  fnessref  36592  neibastop2lem  36595  topmeet  36599  fnejoin2  36604  tailfb  36612  filnetlem4  36616  onsucsuccmpi  36678  ttcwf2  36760  ttcexg  36767  bj-snglss  37330  bj-elpwgALT  37414  bj-restpw  37457  bj-imdirco  37557  dissneqlem  37709  relowlssretop  37732  relowlpssretop  37733  ctbssinf  37775  pibt2  37786  matunitlindflem1  37990  ptrecube  37994  poimirlem29  38023  mblfinlem2  38032  mblfinlem3  38033  mblfinlem4  38034  ismblfin  38035  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  indexa  38107  indexdom  38108  neificl  38127  istotbnd3  38145  sstotbnd2  38148  sstotbnd  38149  equivtotbnd  38152  ssbnd  38162  heiborlem1  38185  heiborlem6  38190  heiborlem8  38192  heiborlem10  38194  unichnidl  38405  pridl  38411  ismaxidl  38414  igenval  38435  igenval2  38440  ispridlc  38444  relcnveq3  38701  iss2  38718  brssr  38955  elrelscnveq3  39001  lsmsat  39507  lssatomic  39510  lssats  39511  lsat0cv  39532  lcvexchlem4  39536  lcvexchlem5  39537  lsatcvatlem  39548  l1cvpat  39553  ispsubsp  40244  linepsubN  40251  pclvalN  40389  ispsubclN  40436  ispsubcl2N  40446  pclfinclN  40449  diaelrnN  41544  docavalN  41622  dochval  41850  dvh4dimat  41937  dochexmidlem1  41959  lpolconN  41986  mapdordlem2  42136  eqresfnbd  42726  ismrcd1  43154  ismrcd2  43155  ismrc  43157  mzpcompact2lem  43207  aomclem6  43511  hbtlem6  43581  onintunirab  43679  rp-brsslt  43874  ssficl  44020  ssuncl  44021  ssdifcl  44022  sssymdifcl  44023  elmapintrab  44027  clcnvlem  44074  iunrelexpmin1  44159  iunrelexpmin2  44163  clsk3nimkb  44491  clsk1indlem1  44496  isotone1  44499  isotone2  44500  ntrclsiso  44518  gneispace  44585  gneispacess2  44597  onfrALTlem5  44993  onfrALTlem5VD  45335  relpfrlem  45404  modelaxreplem1  45429  islptre  46071  dvmptconst  46365  dvmptidg  46367  dvmulcncf  46375  dvdivcncf  46377  dvmptfprod  46395  stoweidlem51  46501  stoweidlem52  46502  fourierdlem103  46659  fourierdlem104  46660  ioorrnopnlem  46754  ioorrnopnxrlem  46756  salgenval  46771  ovnval2  46995  ovncvrrp  47014  ovnsubaddlem1  47020  ovnsubadd  47022  ovncvr2  47061  hspmbl  47079  elsetpreimafvssdm  47868  isubgredg  48364  uhgrimisgrgriclem  48428  grimedg  48433  grtrissvtx  48442  grtrimap  48446  stgredgiun  48456  isubgr3stgrlem6  48469  isubgr3stgrlem7  48470  uspgrlimlem1  48486  uspgrlimlem2  48487  uspgrlimlem3  48488  uspgrlimlem4  48489  clnbgrvtxedg  48492  grlimedgclnbgr  48493  grlimpredg  48496  grlimprclnbgrvtx  48497  grlimgredgex  48498  grlimgrtrilem1  48499  grlimgrtrilem2  48500  grlimgrtri  48501  usgrexmpl1lem  48519  usgrexmpl2lem  48524  uspgrsprfo  48646  unilbss  49315  sepfsepc  49425  unilbeu  49482  ipolubdm  49484  ipoglbdm  49487  discsubc  49561  iinfconstbas  49563  setrec1lem1  50184  setrec1lem4  50187  setrec2fun  50189  elsetrecslem  50196  elpglem2  50209