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	2	adantl 482	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3929	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
5	4	adantr 481	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
6	3, 5	impbid 211	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
7	1, 6	sylbi 216	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  sseq12  3949  sseq1i  3950  sseq1d  3953  nssne2  3983  psseq1  4023  uneqdifeq  4424  sbss  4454  pwjust  4535  elpwg  4537  elpwOLD  4540  elpwgOLD  4541  pwpw0  4747  sssn  4760  ssunsn2  4761  pwsnOLD  4833  unimax  4878  trss  5201  al0ssb  5233  sseliALT  5234  elssabg  5261  intabs  5267  vpwex  5301  nnullss  5378  exss  5379  friOLD  5551  releq  5688  iss  5946  relcnvtrg  6174  fununi  6516  ssimaex  6862  isofrlem  7220  onssmin  7651  tfis  7710  tfisi  7714  funcnvuni  7787  ffoss  7797  f1oweALT  7824  frxp  7976  frrlem1  8111  frrlem13  8123  wfrlem1OLD  8148  wfrlem4OLD  8152  wfrlem15OLD  8163  tfrlem1  8216  oawordeu  8395  qsss  8576  boxcutc  8738  sbthlem2  8880  sbth  8889  findcard2d  8958  ssfi  8965  sbthfi  8994  php  9002  phpOLD  9014  isinf  9045  unbnn2  9080  domunfican  9096  fiint  9100  finsschain  9135  indexfi  9136  dffi3  9199  hartogslem1  9310  cantnfval2  9436  cantnfle  9438  cantnflem1  9456  tz9.1  9496  setind  9501  tcvalg  9505  frmin  9516  scott0  9653  bnd2  9660  carduni  9748  cardaleph  9854  alephinit  9860  aceq3lem  9885  dfac12lem3  9910  infmap2  9983  cflem  10011  cflm  10015  cflecard  10018  cfeq0  10021  cfsuc  10022  cfflb  10024  cfslb  10031  cfslb2n  10033  coftr  10038  fin23lem13  10097  fin23lem16  10100  fin23lem19  10101  fin23lem29  10106  fin1a2lem13  10177  itunitc  10186  domtriomlem  10207  axdc3lem2  10216  zorn2lem7  10267  zornn0g  10270  fpwwe2lem4  10399  pwfseqlem4a  10426  pwfseqlem4  10427  wunfi  10486  wunex2  10503  wuncval  10507  rankcf  10542  tskuni  10548  axgroth6  10593  axgroth3  10596  axgroth4  10597  fzoss1  13423  fsuppmapnn0fiubex  13721  hashf1lem2  14179  cleq1lem  14702  rtrclreclem4  14781  sumeq1  15409  fsumcvg3  15450  fsum2d  15492  fsumabs  15522  fsumrlim  15532  fsumo1  15533  fsumiun  15542  prodeq1f  15627  fprod2d  15700  lcmfunsnlem  16355  coprmprod  16375  vdwmc  16688  prmgaplem3  16763  prmgaplem4  16764  restsspw  17151  ismred2  17321  mrcval  17328  mrcuni  17339  acsfn  17377  isssc  17541  drsdirfi  18032  ipodrsima  18268  cntzssv  18943  pmtrfrn  19075  pmtrrn2  19077  pmtrdifellem1  19093  pmtrdifellem2  19094  sylow2alem2  19232  sylow2a  19233  efgval  19332  gsumzaddlem  19531  ablfac1eulem  19684  lspval  20246  lspindpi  20403  znf1o  20768  zntoslem  20773  aspval  21086  mplsubglem  21214  mpllsslem  21215  mplcoe1  21247  mplcoe5  21250  mdetunilem9  21778  uniopn  22055  fiinopn  22059  fiinbas  22111  baspartn  22113  eltg2  22117  eltg3  22121  topbas  22131  pptbas  22167  clsval  22197  neiint  22264  neips  22273  opnneissb  22274  opnssneib  22275  innei  22285  neiptoptop  22291  neiptopnei  22292  restbas  22318  restcld  22332  neitr  22340  restcls  22341  restntr  22342  cnpdis  22453  cmpsublem  22559  cmpsub  22560  fiuncmp  22564  unconn  22589  1stcfb  22605  2ndc1stc  22611  1stcrest  22613  2ndcctbss  22615  2ndcomap  22618  dis2ndc  22620  lly1stc  22656  refssex  22671  refun0  22675  llycmpkgen2  22710  txbas  22727  eltx  22728  ptuni2  22736  neitx  22767  ptpjopn  22772  ptcld  22773  txlm  22808  tx1stc  22810  txkgen  22812  xkopt  22815  xkococnlem  22819  ptcmpfi  22973  fbssfi  22997  opnfbas  23002  isfil2  23016  isfildlem  23017  snfil  23024  fsubbas  23027  ssfg  23032  fgss2  23034  fgcl  23038  fbasrn  23044  fgtr  23050  ufli  23074  uffix  23081  rnelfmlem  23112  fclscf  23185  alexsublem  23204  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALTlem4  23210  alexsubALT  23211  tmdgsum2  23256  subgntr  23267  opnsubg  23268  qustgpopn  23280  tsmsfbas  23288  tsmsgsum  23299  tsmsres  23304  tsmsf1o  23305  tsmsxplem1  23313  tsmsxp  23315  isust  23364  ustssel  23366  ustincl  23368  ustdiag  23369  ustinvel  23370  ustexhalf  23371  ustexsym  23376  ust0  23380  restutop  23398  ustuqtop4  23405  utopsnneiplem  23408  blssexps  23588  blssex  23589  neibl  23666  blcld  23670  met1stc  23686  met2ndci  23687  metrest  23689  prdsxmslem2  23694  metustfbas  23722  cfilucfil  23724  metuel2  23730  metustbl  23731  restmetu  23735  dscopn  23738  isngp2  23762  tgioo  23968  tgqioo  23972  zdis  23988  xrge0tsms  24006  fsumcn  24042  volivth  24780  vitalilem2  24782  itgfsum  25000  limcun  25068  recnprss  25077  dvmptfsum  25148  ftc1a  25210  plyssc  25370  efopn  25822  jensen  26147  tglnunirn  26918  lpvtx  27447  umgredgprv  27486  usgredgprvALT  27571  issubgr2  27648  subgrprop2  27650  egrsubgr  27653  0uhgrsubgr  27655  frcond3  28642  hhsssh  29640  shintcl  29701  chintcl  29703  spanval  29704  omlsi  29775  pjoml  29807  chnlen0  29815  chsscon3  29871  chlejb1  29883  chnle  29885  spanun  29916  h1datom  29953  cmbr4i  29972  pjoml2  29982  pjoml3  29983  lecm  29988  osumcor2i  30015  osum  30016  spansncv  30024  pjcjt2  30063  pjopyth  30091  hstel2  30590  stj  30606  stcltr1i  30645  mdi  30666  mdbr3  30668  mdbr4  30669  dmdbr  30670  dmdmd  30671  dmdbr5  30679  mdsl1i  30692  mdslmd1lem3  30698  mdslmd1lem4  30699  mdslmd1i  30700  csmdsymi  30705  atss  30717  atom1d  30724  superpos  30725  chcv1  30726  shatomici  30729  shatomistici  30732  hatomistici  30733  chrelat2  30741  chirredi  30765  atcvat4i  30768  mdsymlem2  30775  mdsymlem6  30779  dmdbr6ati  30794  dmdbr7ati  30795  xrge0tsmsd  31326  gsumle  31359  gsumvsca1  31488  gsumvsca2  31489  prmidl  31624  ismxidl  31643  zarcls1  31828  zarclsun  31829  zarclsiin  31830  zarclsint  31831  zarclssn  31832  zartop  31835  zartopon  31836  zart0  31838  zarmxt1  31839  zarcmp  31841  rhmpreimacnlem  31843  rhmpreimacn  31844  tpr2rico  31871  issiga  32089  isrnsiga  32090  sigagenval  32117  measiuns  32194  dya2icoseg  32253  dya2iocnrect  32257  dya2iocuni  32259  carsgmon  32290  carsgsigalem  32291  carsgclctunlem2  32295  carsgclctun  32297  pmeasmono  32300  pmeasadd  32301  bnj517  32874  bnj1118  32973  bnj1145  32982  bnj1154  32988  bnj1452  33041  bnj1498  33050  fineqvpow  33074  fineqvac  33075  fineqvacALT  33076  pthhashvtx  33098  kur14lem1  33177  cvmopnlem  33249  dfon2lem3  33770  dfon2lem7  33774  frxp2  33800  frxp3  33806  brsslt  33989  madef  34049  brsset  34200  fness  34547  fneref  34548  fnessref  34555  neibastop2lem  34558  topmeet  34562  fnejoin2  34567  tailfb  34575  filnetlem4  34579  onsucsuccmpi  34641  bj-snglss  35169  bj-restpw  35272  bj-imdirco  35370  dissneqlem  35520  relowlssretop  35543  relowlpssretop  35544  ctbssinf  35586  pibt2  35597  matunitlindflem1  35782  ptrecube  35786  poimirlem29  35815  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  indexa  35900  indexdom  35901  neificl  35920  istotbnd3  35938  sstotbnd2  35941  sstotbnd  35942  equivtotbnd  35945  ssbnd  35955  heiborlem1  35978  heiborlem6  35983  heiborlem8  35985  heiborlem10  35987  unichnidl  36198  pridl  36204  ismaxidl  36207  igenval  36228  igenval2  36233  ispridlc  36237  relcnveq3  36463  iss2  36486  elrelscnveq3  36616  brssr  36626  lsmsat  37029  lssatomic  37032  lssats  37033  lsat0cv  37054  lcvexchlem4  37058  lcvexchlem5  37059  lsatcvatlem  37070  l1cvpat  37075  ispsubsp  37766  linepsubN  37773  pclvalN  37911  ispsubclN  37958  ispsubcl2N  37968  pclfinclN  37971  diaelrnN  39066  docavalN  39144  dochval  39372  dvh4dimat  39459  dochexmidlem1  39481  lpolconN  39508  mapdordlem2  39658  ismrcd1  40527  ismrcd2  40528  ismrc  40530  mzpcompact2lem  40580  aomclem6  40891  hbtlem6  40961  rgspnval  41000  ssficl  41183  ssuncl  41184  ssdifcl  41185  sssymdifcl  41186  elmapintrab  41191  clcnvlem  41238  iunrelexpmin1  41323  iunrelexpmin2  41327  clsk3nimkb  41657  clsk1indlem1  41662  isotone1  41665  isotone2  41666  ntrclsiso  41684  gneispace  41751  gneispacess2  41763  onfrALTlem5  42169  onfrALTlem5VD  42512  islptre  43167  dvmptconst  43463  dvmptidg  43465  dvmulcncf  43473  dvdivcncf  43475  dvmptfprod  43493  stoweidlem51  43599  stoweidlem52  43600  fourierdlem103  43757  fourierdlem104  43758  ioorrnopnlem  43852  ioorrnopnxrlem  43854  salgenval  43869  ovnval2  44090  ovncvrrp  44109  ovnsubaddlem1  44115  ovnsubadd  44117  ovncvr2  44156  hspmbl  44174  elsetpreimafvssdm  44849  uspgrsprfo  45321  unilbss  46174  sepfsepc  46232  unilbeu  46282  ipolubdm  46284  ipoglbdm  46287  setrec1lem1  46404  setrec1lem4  46407  setrec2fun  46409  elsetrecslem  46415  elpglem2  46428