Theorem sseq1 3933

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 3923	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3915	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3915	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	2, 3	anbiim 653	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
5	4	ancoms 464	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
6	1, 5	sylbi 220	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  sseq12  3935  sseq1i  3936  sseq1d  3939  nssne2  3971  psseq1  4017  vvin  4358  uneqdifeq  4447  sbss  4475  pwjust  4557  elpwg  4559  pwpw0  4773  sssn  4786  ssunsn2  4787  unimax  4904  trss  5221  al0ssb  5261  sseliALT  5262  elssabg  5303  intabs  5309  vpwex  5338  nnullss  5429  exss  5430  releq  5752  iss  6026  relcnvtrgOLD  6269  fununi  6615  ssimaex  6970  isofrlem  7348  onssmin  7806  tfis  7866  tfisi  7870  funcnvuni  7944  ffoss  7958  f1oweALT  7984  frxp  8138  frxp2  8161  frrlem1  8304  frrlem13  8316  tfrlem1  8383  oawordeu  8563  coflton  8680  cofon1  8681  cofon2  8682  naddunif  8703  qsss  8796  boxcutc  8969  sbthlem2  9107  sbth  9116  findcard2d  9182  ssfi  9188  sbthfi  9214  php  9222  isinf  9256  unbnn2  9289  domunfican  9313  fiint  9318  finsschain  9348  indexfi  9349  dffi3  9423  hartogslem1  9536  cantnfval2  9670  cantnfle  9672  cantnflem1  9690  tz9.1  9730  tcvalg  9737  setind  9748  frmin  9753  scott0b  9937  scott0OLD  9938  bnd2  9956  setrec1lem1  9966  setrec1lem4  9971  setrec2fun  9973  carduni  10062  cardaleph  10168  alephinit  10174  aceq3lem  10199  dfac12lem3  10224  infmap2  10295  cflem  10323  cflm  10327  cflecard  10330  cfeq0  10334  cfsuc  10335  cfflb  10337  cfslb  10344  cfslb2n  10346  coftr  10351  fin23lem13  10410  fin23lem16  10413  fin23lem19  10414  fin23lem29  10419  fin1a2lem13  10490  itunitc  10499  domtriomlem  10520  axdc3lem2  10529  zorn2lem7  10580  zornn0g  10583  pwfseqlem4a  10746  pwfseqlem4  10747  wunfi  10806  wunex2  10823  wuncval  10827  rankcf  10862  tskuni  10868  axgroth6  10913  axgroth3  10916  axgroth4  10917  fzoss1  13821  fsuppmapnn0fiubex  14135  hashf1lem2  14601  cleq1lem  15135  rtrclreclem4  15214  sumeq1  15856  fsumcvg3  15895  fsum2d  15937  fsumabs  15968  fsumrlim  15978  fsumo1  15979  fsumiun  15988  prodeq1f  16075  prodeq1  16076  fprod2d  16148  lcmfunsnlem  16816  coprmprod  16836  vdwmc  17156  prmgaplem3  17231  prmgaplem4  17232  restsspw  17602  ismred2  17773  mrcval  17784  mrcuni  17795  acsfn  17833  isssc  17995  drsdirfi  18479  ipodrsima  18715  cntzssv  19542  pmtrfrn  19672  pmtrrn2  19674  pmtrdifellem1  19690  pmtrdifellem2  19691  sylow2alem2  19832  sylow2a  19833  efgval  19931  gsumzaddlem  20135  ablfac1eulem  20288  gsumle  20359  rgspnval  20864  lspval  21250  lspindpi  21410  unichnlidl  21516  rspprop  21524  prmidl  21621  znf1o  21857  zntoslem  21862  aspval  22180  mplsubglem  22306  mpllsslem  22307  mplcoe1  22346  mplcoe5  22349  mdetunilem9  22935  matunitlindflem1  22994  uniopn  23215  fiinopn  23219  fiinbas  23270  baspartn  23272  eltg2  23276  eltg3  23280  topbas  23290  pptbas  23326  clsval  23355  neiint  23422  neips  23431  opnneissb  23432  opnssneib  23433  innei  23443  neiptoptop  23449  neiptopnei  23450  restbas  23476  restcld  23490  neitr  23498  restcls  23499  restntr  23500  cnpdis  23611  cmpsublem  23717  cmpsub  23718  fiuncmp  23722  unconn  23747  1stcfb  23763  2ndc1stc  23769  1stcrest  23771  2ndcctbss  23774  2ndcomap  23777  dis2ndc  23779  lly1stc  23815  refssex  23830  refun0  23834  llycmpkgen2  23869  txbas  23886  eltx  23887  ptuni2  23895  neitx  23926  ptpjopn  23931  ptcld  23932  txlm  23967  tx1stc  23969  txkgen  23971  xkopt  23974  xkococnlem  23978  ptcmpfi  24132  fbssfi  24156  opnfbas  24161  isfil2  24175  isfildlem  24176  snfil  24183  fsubbas  24186  ssfg  24191  fgss2  24193  fgcl  24197  fbasrn  24203  fgtr  24209  ufli  24233  uffix  24240  rnelfmlem  24271  fclscf  24344  alexsublem  24363  alexsubALTlem2  24367  alexsubALTlem3  24368  alexsubALTlem4  24369  alexsubALT  24370  tmdgsum2  24415  subgntr  24426  opnsubg  24427  qustgpopn  24439  tsmsfbas  24447  tsmsgsum  24458  tsmsres  24463  tsmsf1o  24464  tsmsxplem1  24472  tsmsxp  24474  isust  24523  ustssel  24525  ustincl  24527  ustdiag  24528  ustinvel  24529  ustexhalf  24530  ustexsym  24535  ust0  24539  restutop  24556  ustuqtop4  24563  utopsnneiplem  24566  blssexps  24745  blssex  24746  neibl  24820  blcld  24824  met1stc  24840  met2ndci  24841  metrest  24843  prdsxmslem2  24848  metustfbas  24876  cfilucfil  24878  metuel2  24884  metustbl  24885  restmetu  24889  dscopn  24892  isngp2  24916  tgioo  25115  tgqioo  25119  zdis  25136  xrge0tsms  25154  fsumcn  25191  volivth  25928  vitalilem2  25930  itgfsum  26147  limcun  26215  recnprss  26224  dvmptfsum  26295  ftc1a  26357  plyssc  26518  efopn  26986  jensen  27316  brslts  28148  madef  28222  tglnunirn  29011  brprlng  29416  lpvtx  29646  umgredgprv  29685  usgredgprvALT  29776  issubgr2  29853  subgrprop2  29855  egrsubgr  29858  0uhgrsubgr  29860  pthhashvtx  30315  frcond3  30870  hhsssh  31871  shintcl  31932  chintcl  31934  spanval  31935  omlsi  32006  pjoml  32038  chnlen0  32046  chsscon3  32102  chlejb1  32114  chnle  32116  spanun  32147  h1datom  32184  cmbr4i  32203  pjoml2  32213  pjoml3  32214  lecm  32219  osumcor2i  32246  osum  32247  spansncv  32255  pjcjt2  32294  pjopyth  32322  hstel2  32821  stj  32837  stcltr1i  32876  mdi  32897  mdbr3  32899  mdbr4  32900  dmdbr  32901  dmdmd  32902  dmdbr5  32910  mdsl1i  32923  mdslmd1lem3  32929  mdslmd1lem4  32930  mdslmd1i  32931  csmdsymi  32936  atss  32948  atom1d  32955  superpos  32956  chcv1  32957  shatomici  32960  shatomistici  32963  hatomistici  32964  chrelat2  32972  chirredi  32996  atcvat4i  32999  mdsymlem2  33006  mdsymlem6  33010  dmdbr6ati  33025  dmdbr7ati  33026  xrge0tsmsd  33634  gsumvsca1  33787  gsumvsca2  33788  ismxidl  33987  constrfiss  34383  zarcls1  34501  zarclsun  34502  zarclsiin  34503  zarclsint  34504  zarclssn  34505  zartop  34508  zartopon  34509  zart0  34511  zarmxt1  34512  zarcmp  34514  rhmpreimacnlem  34516  rhmpreimacn  34517  tpr2rico  34544  issiga  34744  isrnsiga  34745  sigagenval  34773  measiuns  34850  dya2icoseg  34909  dya2iocnrect  34913  dya2iocuni  34915  carsgmon  34946  carsgsigalem  34947  carsgclctunlem2  34951  carsgclctun  34953  pmeasmono  34956  pmeasadd  34957  bnj517  35515  bnj1118  35614  bnj1145  35623  bnj1154  35629  bnj1452  35682  bnj1498  35691  rankscottu  35753  weexenwe  35756  acwer1prclem  35759  fineqvpow  35783  fineqvac  35784  fineqvacALT  35785  setindregs  35798  tz9.1regs  35802  fineqvr1ombregs  35806  rankkardu  35839  vonf1wev  35887  vonf1owevOLD  35889  onprcf1acwevdlem1  35895  kur14lem1  35971  cvmopnlem  36043  dfon2lem3  36547  dfon2lem7  36551  brsset  36651  fness  37137  fneref  37138  fnessref  37145  neibastop2lem  37148  topmeet  37152  fnejoin2  37157  tailfb  37165  filnetlem4  37169  onsucsuccmpi  37231  ttcwf2  37313  ttcexg  37320  bj-snglss  37883  bj-elpwgALT  37969  bj-restpw  38013  bj-imdirco  38112  dissneqlem  38264  relowlssretop  38287  relowlpssretop  38288  ctbssinf  38330  pibt2  38341  ptrecube  38539  poimirlem29  38568  mblfinlem2  38577  mblfinlem3  38578  mblfinlem4  38579  ismblfin  38580  ovoliunnfl  38581  voliunnfl  38583  volsupnfl  38584  indexa  38668  indexdom  38669  neificl  38688  istotbnd3  38706  sstotbnd2  38709  sstotbnd  38710  equivtotbnd  38713  ssbnd  38723  heiborlem1  38746  heiborlem6  38751  heiborlem8  38753  heiborlem10  38755  unichnidl  38966  pridl  38972  ismaxidl  38975  igenval  38996  igenval2  39001  ispridlc  39005  relcnveq3  39260  iss2  39277  brssr  39514  elrelscnveq3  39560  lsmsat  40066  lssatomic  40069  lssats  40070  lsat0cv  40091  lcvexchlem4  40095  lcvexchlem5  40096  lsatcvatlem  40107  l1cvpat  40112  ispsubsp  40803  linepsubN  40810  pclvalN  40948  ispsubclN  40995  ispsubcl2N  41005  pclfinclN  41008  diaelrnN  42103  docavalN  42181  dochval  42409  dvh4dimat  42496  dochexmidlem1  42518  lpolconN  42545  mapdordlem2  42695  eqresfnbd  43287  ismrcd1  43709  ismrcd2  43710  ismrc  43712  mzpcompact2lem  43762  aomclem6  44061  hbtlem6  44131  onintunirab  44229  rp-brsslt  44424  ssficl  44570  ssuncl  44571  ssdifcl  44572  sssymdifcl  44573  elmapintrab  44577  clcnvlem  44623  iunrelexpmin1  44708  iunrelexpmin2  44712  clsk3nimkb  45040  clsk1indlem1  45045  isotone1  45048  isotone2  45049  ntrclsiso  45067  gneispace  45134  gneispacess2  45146  onfrALTlem5  45525  onfrALTlem5VD  45867  relpfrlem  45943  modelaxreplem1  45968  islptre  46631  dvmptconst  46925  dvmptidg  46927  dvmulcncf  46935  dvdivcncf  46937  dvmptfprod  46955  stoweidlem51  47061  stoweidlem52  47062  fourierdlem103  47219  fourierdlem104  47220  ioorrnopnlem  47314  ioorrnopnxrlem  47316  salgenval  47331  ovnval2  47555  ovncvrrp  47574  ovnsubaddlem1  47580  ovnsubadd  47582  ovncvr2  47621  hspmbl  47639  elsetpreimafvssdm  48468  isubgredg  48964  uhgrimisgrgriclem  49028  grimedg  49033  grtrissvtx  49042  grtrimap  49046  stgredgiun  49056  isubgr3stgrlem6  49069  isubgr3stgrlem7  49070  uspgrlimlem1  49086  uspgrlimlem2  49087  uspgrlimlem3  49088  uspgrlimlem4  49089  clnbgrvtxedg  49092  grlimedgclnbgr  49093  grlimpredg  49096  grlimprclnbgrvtx  49097  grlimgredgex  49098  grlimgrtrilem1  49099  grlimgrtrilem2  49100  grlimgrtri  49101  usgrexmpl1lem  49119  usgrexmpl2lem  49124  uspgrsprfo  49246  unilbss  49928  sepfsepc  50036  unilbeu  50093  ipolubdm  50095  ipoglbdm  50098  discsubc  50172  iinfconstbas  50174  elsetrecslem  50792  elpglem2  50805