Theorem sseq1 3972

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 3962	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3954	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 482	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3954	. . . 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 1541   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  sseq12  3974  sseq1i  3975  sseq1d  3978  nssne2  4010  psseq1  4052  uneqdifeq  4455  sbss  4485  pwjust  4566  elpwg  4568  pwpw0  4778  sssn  4791  ssunsn2  4792  pwsnOLD  4863  unimax  4910  trss  5238  al0ssb  5270  sseliALT  5271  elssabg  5298  intabs  5304  vpwex  5337  nnullss  5424  exss  5425  friOLD  5599  releq  5737  iss  5994  relcnvtrg  6223  fununi  6581  ssimaex  6931  isofrlem  7290  onssmin  7732  tfis  7796  tfisi  7800  funcnvuni  7873  ffoss  7883  f1oweALT  7910  frxp  8063  frxp2  8081  frrlem1  8222  frrlem13  8234  wfrlem1OLD  8259  wfrlem4OLD  8263  wfrlem15OLD  8274  tfrlem1  8327  oawordeu  8507  coflton  8622  cofon1  8623  cofon2  8624  naddunif  8644  qsss  8724  boxcutc  8886  sbthlem2  9035  sbth  9044  findcard2d  9117  ssfi  9124  sbthfi  9153  php  9161  phpOLD  9173  isinf  9211  isinfOLD  9212  unbnn2  9251  domunfican  9271  fiint  9275  finsschain  9310  indexfi  9311  dffi3  9376  hartogslem1  9487  cantnfval2  9614  cantnfle  9616  cantnflem1  9634  tz9.1  9674  setind  9679  tcvalg  9683  frmin  9694  scott0  9831  bnd2  9838  carduni  9926  cardaleph  10034  alephinit  10040  aceq3lem  10065  dfac12lem3  10090  infmap2  10163  cflem  10191  cflm  10195  cflecard  10198  cfeq0  10201  cfsuc  10202  cfflb  10204  cfslb  10211  cfslb2n  10213  coftr  10218  fin23lem13  10277  fin23lem16  10280  fin23lem19  10281  fin23lem29  10286  fin1a2lem13  10357  itunitc  10366  domtriomlem  10387  axdc3lem2  10396  zorn2lem7  10447  zornn0g  10450  fpwwe2lem4  10579  pwfseqlem4a  10606  pwfseqlem4  10607  wunfi  10666  wunex2  10683  wuncval  10687  rankcf  10722  tskuni  10728  axgroth6  10773  axgroth3  10776  axgroth4  10777  fzoss1  13609  fsuppmapnn0fiubex  13907  hashf1lem2  14367  cleq1lem  14879  rtrclreclem4  14958  sumeq1  15585  fsumcvg3  15625  fsum2d  15667  fsumabs  15697  fsumrlim  15707  fsumo1  15708  fsumiun  15717  prodeq1f  15802  fprod2d  15875  lcmfunsnlem  16528  coprmprod  16548  vdwmc  16861  prmgaplem3  16936  prmgaplem4  16937  restsspw  17327  ismred2  17497  mrcval  17504  mrcuni  17515  acsfn  17553  isssc  17717  drsdirfi  18208  ipodrsima  18444  cntzssv  19122  pmtrfrn  19254  pmtrrn2  19256  pmtrdifellem1  19272  pmtrdifellem2  19273  sylow2alem2  19414  sylow2a  19415  efgval  19513  gsumzaddlem  19712  ablfac1eulem  19865  lspval  20493  lspindpi  20652  znf1o  20995  zntoslem  21000  aspval  21313  mplsubglem  21442  mpllsslem  21443  mplcoe1  21475  mplcoe5  21478  mdetunilem9  22006  uniopn  22283  fiinopn  22287  fiinbas  22339  baspartn  22341  eltg2  22345  eltg3  22349  topbas  22359  pptbas  22395  clsval  22425  neiint  22492  neips  22501  opnneissb  22502  opnssneib  22503  innei  22513  neiptoptop  22519  neiptopnei  22520  restbas  22546  restcld  22560  neitr  22568  restcls  22569  restntr  22570  cnpdis  22681  cmpsublem  22787  cmpsub  22788  fiuncmp  22792  unconn  22817  1stcfb  22833  2ndc1stc  22839  1stcrest  22841  2ndcctbss  22843  2ndcomap  22846  dis2ndc  22848  lly1stc  22884  refssex  22899  refun0  22903  llycmpkgen2  22938  txbas  22955  eltx  22956  ptuni2  22964  neitx  22995  ptpjopn  23000  ptcld  23001  txlm  23036  tx1stc  23038  txkgen  23040  xkopt  23043  xkococnlem  23047  ptcmpfi  23201  fbssfi  23225  opnfbas  23230  isfil2  23244  isfildlem  23245  snfil  23252  fsubbas  23255  ssfg  23260  fgss2  23262  fgcl  23266  fbasrn  23272  fgtr  23278  ufli  23302  uffix  23309  rnelfmlem  23340  fclscf  23413  alexsublem  23432  alexsubALTlem2  23436  alexsubALTlem3  23437  alexsubALTlem4  23438  alexsubALT  23439  tmdgsum2  23484  subgntr  23495  opnsubg  23496  qustgpopn  23508  tsmsfbas  23516  tsmsgsum  23527  tsmsres  23532  tsmsf1o  23533  tsmsxplem1  23541  tsmsxp  23543  isust  23592  ustssel  23594  ustincl  23596  ustdiag  23597  ustinvel  23598  ustexhalf  23599  ustexsym  23604  ust0  23608  restutop  23626  ustuqtop4  23633  utopsnneiplem  23636  blssexps  23816  blssex  23817  neibl  23894  blcld  23898  met1stc  23914  met2ndci  23915  metrest  23917  prdsxmslem2  23922  metustfbas  23950  cfilucfil  23952  metuel2  23958  metustbl  23959  restmetu  23963  dscopn  23966  isngp2  23990  tgioo  24196  tgqioo  24200  zdis  24216  xrge0tsms  24234  fsumcn  24270  volivth  25008  vitalilem2  25010  itgfsum  25228  limcun  25296  recnprss  25305  dvmptfsum  25376  ftc1a  25438  plyssc  25598  efopn  26050  jensen  26375  brsslt  27168  madef  27229  tglnunirn  27553  lpvtx  28082  umgredgprv  28121  usgredgprvALT  28206  issubgr2  28283  subgrprop2  28285  egrsubgr  28288  0uhgrsubgr  28290  frcond3  29276  hhsssh  30274  shintcl  30335  chintcl  30337  spanval  30338  omlsi  30409  pjoml  30441  chnlen0  30449  chsscon3  30505  chlejb1  30517  chnle  30519  spanun  30550  h1datom  30587  cmbr4i  30606  pjoml2  30616  pjoml3  30617  lecm  30622  osumcor2i  30649  osum  30650  spansncv  30658  pjcjt2  30697  pjopyth  30725  hstel2  31224  stj  31240  stcltr1i  31279  mdi  31300  mdbr3  31302  mdbr4  31303  dmdbr  31304  dmdmd  31305  dmdbr5  31313  mdsl1i  31326  mdslmd1lem3  31332  mdslmd1lem4  31333  mdslmd1i  31334  csmdsymi  31339  atss  31351  atom1d  31358  superpos  31359  chcv1  31360  shatomici  31363  shatomistici  31366  hatomistici  31367  chrelat2  31375  chirredi  31399  atcvat4i  31402  mdsymlem2  31409  mdsymlem6  31413  dmdbr6ati  31428  dmdbr7ati  31429  xrge0tsmsd  31969  gsumle  32002  gsumvsca1  32131  gsumvsca2  32132  prmidl  32288  ismxidl  32307  zarcls1  32539  zarclsun  32540  zarclsiin  32541  zarclsint  32542  zarclssn  32543  zartop  32546  zartopon  32547  zart0  32549  zarmxt1  32550  zarcmp  32552  rhmpreimacnlem  32554  rhmpreimacn  32555  tpr2rico  32582  issiga  32800  isrnsiga  32801  sigagenval  32828  measiuns  32905  dya2icoseg  32966  dya2iocnrect  32970  dya2iocuni  32972  carsgmon  33003  carsgsigalem  33004  carsgclctunlem2  33008  carsgclctun  33010  pmeasmono  33013  pmeasadd  33014  bnj517  33586  bnj1118  33685  bnj1145  33694  bnj1154  33700  bnj1452  33753  bnj1498  33762  fineqvpow  33786  fineqvac  33787  fineqvacALT  33788  pthhashvtx  33808  kur14lem1  33887  cvmopnlem  33959  dfon2lem3  34446  dfon2lem7  34450  brsset  34550  fness  34897  fneref  34898  fnessref  34905  neibastop2lem  34908  topmeet  34912  fnejoin2  34917  tailfb  34925  filnetlem4  34929  onsucsuccmpi  34991  bj-snglss  35514  bj-elpwgALT  35598  bj-restpw  35636  bj-imdirco  35734  dissneqlem  35884  relowlssretop  35907  relowlpssretop  35908  ctbssinf  35950  pibt2  35961  matunitlindflem1  36147  ptrecube  36151  poimirlem29  36180  mblfinlem2  36189  mblfinlem3  36190  mblfinlem4  36191  ismblfin  36192  ovoliunnfl  36193  voliunnfl  36195  volsupnfl  36196  indexa  36265  indexdom  36266  neificl  36285  istotbnd3  36303  sstotbnd2  36306  sstotbnd  36307  equivtotbnd  36310  ssbnd  36320  heiborlem1  36343  heiborlem6  36348  heiborlem8  36350  heiborlem10  36352  unichnidl  36563  pridl  36569  ismaxidl  36572  igenval  36593  igenval2  36598  ispridlc  36602  relcnveq3  36855  iss2  36878  elrelscnveq3  37026  brssr  37036  lsmsat  37543  lssatomic  37546  lssats  37547  lsat0cv  37568  lcvexchlem4  37572  lcvexchlem5  37573  lsatcvatlem  37584  l1cvpat  37589  ispsubsp  38281  linepsubN  38288  pclvalN  38426  ispsubclN  38473  ispsubcl2N  38483  pclfinclN  38486  diaelrnN  39581  docavalN  39659  dochval  39887  dvh4dimat  39974  dochexmidlem1  39996  lpolconN  40023  mapdordlem2  40173  ismrcd1  41079  ismrcd2  41080  ismrc  41082  mzpcompact2lem  41132  aomclem6  41444  hbtlem6  41514  rgspnval  41553  onintunirab  41619  rp-brsslt  41817  ssficl  41963  ssuncl  41964  ssdifcl  41965  sssymdifcl  41966  elmapintrab  41970  clcnvlem  42017  iunrelexpmin1  42102  iunrelexpmin2  42106  clsk3nimkb  42434  clsk1indlem1  42439  isotone1  42442  isotone2  42443  ntrclsiso  42461  gneispace  42528  gneispacess2  42540  onfrALTlem5  42946  onfrALTlem5VD  43289  islptre  43980  dvmptconst  44276  dvmptidg  44278  dvmulcncf  44286  dvdivcncf  44288  dvmptfprod  44306  stoweidlem51  44412  stoweidlem52  44413  fourierdlem103  44570  fourierdlem104  44571  ioorrnopnlem  44665  ioorrnopnxrlem  44667  salgenval  44682  ovnval2  44906  ovncvrrp  44925  ovnsubaddlem1  44931  ovnsubadd  44933  ovncvr2  44972  hspmbl  44990  elsetpreimafvssdm  45698  uspgrsprfo  46170  unilbss  47022  sepfsepc  47080  unilbeu  47130  ipolubdm  47132  ipoglbdm  47135  setrec1lem1  47252  setrec1lem4  47255  setrec2fun  47257  elsetrecslem  47264  elpglem2  47277