Theorem sseq1 4008

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ⊆ wss 3949

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sseq12  4010  sseq1i  4011  sseq1d  4014  nssne2  4046  psseq1  4088  uneqdifeq  4493  sbss  4523  pwjust  4604  elpwg  4606  pwpw0  4817  sssn  4830  ssunsn2  4831  pwsnOLD  4902  unimax  4949  trss  5277  al0ssb  5309  sseliALT  5310  elssabg  5337  intabs  5343  vpwex  5376  nnullss  5463  exss  5464  friOLD  5638  releq  5777  iss  6036  relcnvtrg  6266  fununi  6624  ssimaex  6977  isofrlem  7337  onssmin  7780  tfis  7844  tfisi  7848  funcnvuni  7922  ffoss  7932  f1oweALT  7959  frxp  8112  frxp2  8130  frrlem1  8271  frrlem13  8283  wfrlem1OLD  8308  wfrlem4OLD  8312  wfrlem15OLD  8323  tfrlem1  8376  oawordeu  8555  coflton  8670  cofon1  8671  cofon2  8672  naddunif  8692  qsss  8772  boxcutc  8935  sbthlem2  9084  sbth  9093  findcard2d  9166  ssfi  9173  sbthfi  9202  php  9210  phpOLD  9222  isinf  9260  isinfOLD  9261  unbnn2  9300  domunfican  9320  fiint  9324  finsschain  9359  indexfi  9360  dffi3  9426  hartogslem1  9537  cantnfval2  9664  cantnfle  9666  cantnflem1  9684  tz9.1  9724  setind  9729  tcvalg  9733  frmin  9744  scott0  9881  bnd2  9888  carduni  9976  cardaleph  10084  alephinit  10090  aceq3lem  10115  dfac12lem3  10140  infmap2  10213  cflem  10241  cflm  10245  cflecard  10248  cfeq0  10251  cfsuc  10252  cfflb  10254  cfslb  10261  cfslb2n  10263  coftr  10268  fin23lem13  10327  fin23lem16  10330  fin23lem19  10331  fin23lem29  10336  fin1a2lem13  10407  itunitc  10416  domtriomlem  10437  axdc3lem2  10446  zorn2lem7  10497  zornn0g  10500  fpwwe2lem4  10629  pwfseqlem4a  10656  pwfseqlem4  10657  wunfi  10716  wunex2  10733  wuncval  10737  rankcf  10772  tskuni  10778  axgroth6  10823  axgroth3  10826  axgroth4  10827  fzoss1  13659  fsuppmapnn0fiubex  13957  hashf1lem2  14417  cleq1lem  14929  rtrclreclem4  15008  sumeq1  15635  fsumcvg3  15675  fsum2d  15717  fsumabs  15747  fsumrlim  15757  fsumo1  15758  fsumiun  15767  prodeq1f  15852  fprod2d  15925  lcmfunsnlem  16578  coprmprod  16598  vdwmc  16911  prmgaplem3  16986  prmgaplem4  16987  restsspw  17377  ismred2  17547  mrcval  17554  mrcuni  17565  acsfn  17603  isssc  17767  drsdirfi  18258  ipodrsima  18494  cntzssv  19192  pmtrfrn  19326  pmtrrn2  19328  pmtrdifellem1  19344  pmtrdifellem2  19345  sylow2alem2  19486  sylow2a  19487  efgval  19585  gsumzaddlem  19789  ablfac1eulem  19942  lspval  20586  lspindpi  20745  znf1o  21107  zntoslem  21112  aspval  21427  mplsubglem  21558  mpllsslem  21559  mplcoe1  21592  mplcoe5  21595  mdetunilem9  22122  uniopn  22399  fiinopn  22403  fiinbas  22455  baspartn  22457  eltg2  22461  eltg3  22465  topbas  22475  pptbas  22511  clsval  22541  neiint  22608  neips  22617  opnneissb  22618  opnssneib  22619  innei  22629  neiptoptop  22635  neiptopnei  22636  restbas  22662  restcld  22676  neitr  22684  restcls  22685  restntr  22686  cnpdis  22797  cmpsublem  22903  cmpsub  22904  fiuncmp  22908  unconn  22933  1stcfb  22949  2ndc1stc  22955  1stcrest  22957  2ndcctbss  22959  2ndcomap  22962  dis2ndc  22964  lly1stc  23000  refssex  23015  refun0  23019  llycmpkgen2  23054  txbas  23071  eltx  23072  ptuni2  23080  neitx  23111  ptpjopn  23116  ptcld  23117  txlm  23152  tx1stc  23154  txkgen  23156  xkopt  23159  xkococnlem  23163  ptcmpfi  23317  fbssfi  23341  opnfbas  23346  isfil2  23360  isfildlem  23361  snfil  23368  fsubbas  23371  ssfg  23376  fgss2  23378  fgcl  23382  fbasrn  23388  fgtr  23394  ufli  23418  uffix  23425  rnelfmlem  23456  fclscf  23529  alexsublem  23548  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  alexsubALT  23555  tmdgsum2  23600  subgntr  23611  opnsubg  23612  qustgpopn  23624  tsmsfbas  23632  tsmsgsum  23643  tsmsres  23648  tsmsf1o  23649  tsmsxplem1  23657  tsmsxp  23659  isust  23708  ustssel  23710  ustincl  23712  ustdiag  23713  ustinvel  23714  ustexhalf  23715  ustexsym  23720  ust0  23724  restutop  23742  ustuqtop4  23749  utopsnneiplem  23752  blssexps  23932  blssex  23933  neibl  24010  blcld  24014  met1stc  24030  met2ndci  24031  metrest  24033  prdsxmslem2  24038  metustfbas  24066  cfilucfil  24068  metuel2  24074  metustbl  24075  restmetu  24079  dscopn  24082  isngp2  24106  tgioo  24312  tgqioo  24316  zdis  24332  xrge0tsms  24350  fsumcn  24386  volivth  25124  vitalilem2  25126  itgfsum  25344  limcun  25412  recnprss  25421  dvmptfsum  25492  ftc1a  25554  plyssc  25714  efopn  26166  jensen  26493  brsslt  27287  madef  27351  tglnunirn  27799  lpvtx  28328  umgredgprv  28367  usgredgprvALT  28452  issubgr2  28529  subgrprop2  28531  egrsubgr  28534  0uhgrsubgr  28536  frcond3  29522  hhsssh  30522  shintcl  30583  chintcl  30585  spanval  30586  omlsi  30657  pjoml  30689  chnlen0  30697  chsscon3  30753  chlejb1  30765  chnle  30767  spanun  30798  h1datom  30835  cmbr4i  30854  pjoml2  30864  pjoml3  30865  lecm  30870  osumcor2i  30897  osum  30898  spansncv  30906  pjcjt2  30945  pjopyth  30973  hstel2  31472  stj  31488  stcltr1i  31527  mdi  31548  mdbr3  31550  mdbr4  31551  dmdbr  31552  dmdmd  31553  dmdbr5  31561  mdsl1i  31574  mdslmd1lem3  31580  mdslmd1lem4  31581  mdslmd1i  31582  csmdsymi  31587  atss  31599  atom1d  31606  superpos  31607  chcv1  31608  shatomici  31611  shatomistici  31614  hatomistici  31615  chrelat2  31623  chirredi  31647  atcvat4i  31650  mdsymlem2  31657  mdsymlem6  31661  dmdbr6ati  31676  dmdbr7ati  31677  xrge0tsmsd  32209  gsumle  32242  gsumvsca1  32371  gsumvsca2  32372  prmidl  32558  ismxidl  32578  zarcls1  32849  zarclsun  32850  zarclsiin  32851  zarclsint  32852  zarclssn  32853  zartop  32856  zartopon  32857  zart0  32859  zarmxt1  32860  zarcmp  32862  rhmpreimacnlem  32864  rhmpreimacn  32865  tpr2rico  32892  issiga  33110  isrnsiga  33111  sigagenval  33138  measiuns  33215  dya2icoseg  33276  dya2iocnrect  33280  dya2iocuni  33282  carsgmon  33313  carsgsigalem  33314  carsgclctunlem2  33318  carsgclctun  33320  pmeasmono  33323  pmeasadd  33324  bnj517  33896  bnj1118  33995  bnj1145  34004  bnj1154  34010  bnj1452  34063  bnj1498  34072  fineqvpow  34096  fineqvac  34097  fineqvacALT  34098  pthhashvtx  34118  kur14lem1  34197  cvmopnlem  34269  dfon2lem3  34757  dfon2lem7  34761  brsset  34861  fness  35234  fneref  35235  fnessref  35242  neibastop2lem  35245  topmeet  35249  fnejoin2  35254  tailfb  35262  filnetlem4  35266  onsucsuccmpi  35328  bj-snglss  35851  bj-elpwgALT  35935  bj-restpw  35973  bj-imdirco  36071  dissneqlem  36221  relowlssretop  36244  relowlpssretop  36245  ctbssinf  36287  pibt2  36298  matunitlindflem1  36484  ptrecube  36488  poimirlem29  36517  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  indexa  36601  indexdom  36602  neificl  36621  istotbnd3  36639  sstotbnd2  36642  sstotbnd  36643  equivtotbnd  36646  ssbnd  36656  heiborlem1  36679  heiborlem6  36684  heiborlem8  36686  heiborlem10  36688  unichnidl  36899  pridl  36905  ismaxidl  36908  igenval  36929  igenval2  36934  ispridlc  36938  relcnveq3  37190  iss2  37213  elrelscnveq3  37361  brssr  37371  lsmsat  37878  lssatomic  37881  lssats  37882  lsat0cv  37903  lcvexchlem4  37907  lcvexchlem5  37908  lsatcvatlem  37919  l1cvpat  37924  ispsubsp  38616  linepsubN  38623  pclvalN  38761  ispsubclN  38808  ispsubcl2N  38818  pclfinclN  38821  diaelrnN  39916  docavalN  39994  dochval  40222  dvh4dimat  40309  dochexmidlem1  40331  lpolconN  40358  mapdordlem2  40508  eqresfnbd  41054  ismrcd1  41436  ismrcd2  41437  ismrc  41439  mzpcompact2lem  41489  aomclem6  41801  hbtlem6  41871  rgspnval  41910  onintunirab  41976  rp-brsslt  42174  ssficl  42320  ssuncl  42321  ssdifcl  42322  sssymdifcl  42323  elmapintrab  42327  clcnvlem  42374  iunrelexpmin1  42459  iunrelexpmin2  42463  clsk3nimkb  42791  clsk1indlem1  42796  isotone1  42799  isotone2  42800  ntrclsiso  42818  gneispace  42885  gneispacess2  42897  onfrALTlem5  43303  onfrALTlem5VD  43646  islptre  44335  dvmptconst  44631  dvmptidg  44633  dvmulcncf  44641  dvdivcncf  44643  dvmptfprod  44661  stoweidlem51  44767  stoweidlem52  44768  fourierdlem103  44925  fourierdlem104  44926  ioorrnopnlem  45020  ioorrnopnxrlem  45022  salgenval  45037  ovnval2  45261  ovncvrrp  45280  ovnsubaddlem1  45286  ovnsubadd  45288  ovncvr2  45327  hspmbl  45345  elsetpreimafvssdm  46054  uspgrsprfo  46526  unilbss  47502  sepfsepc  47560  unilbeu  47610  ipolubdm  47612  ipoglbdm  47615  setrec1lem1  47732  setrec1lem4  47735  setrec2fun  47737  elsetrecslem  47744  elpglem2  47757