Theorem sseq1 4034

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 4024	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 4015	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 481	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 4015	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
5	4	adantr 480	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
6	3, 5	impbid 212	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
7	1, 6	sylbi 217	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  sseq12  4036  sseq1i  4037  sseq1d  4040  nssne2  4072  psseq1  4113  uneqdifeq  4516  sbss  4542  pwjust  4623  elpwg  4625  pwpw0  4838  sssn  4851  ssunsn2  4852  unimax  4968  trss  5294  al0ssb  5326  sseliALT  5327  elssabg  5361  intabs  5367  vpwex  5395  nnullss  5482  exss  5483  friOLD  5658  releq  5800  iss  6064  relcnvtrg  6297  fununi  6653  ssimaex  7007  isofrlem  7376  onssmin  7828  tfis  7892  tfisi  7896  funcnvuni  7972  ffoss  7986  f1oweALT  8013  frxp  8167  frxp2  8185  frrlem1  8327  frrlem13  8339  wfrlem1OLD  8364  wfrlem4OLD  8368  wfrlem15OLD  8379  tfrlem1  8432  oawordeu  8611  coflton  8727  cofon1  8728  cofon2  8729  naddunif  8749  qsss  8836  boxcutc  8999  sbthlem2  9150  sbth  9159  findcard2d  9232  ssfi  9240  sbthfi  9265  php  9273  phpOLD  9285  isinf  9323  isinfOLD  9324  unbnn2  9361  domunfican  9389  fiint  9394  fiintOLD  9395  finsschain  9429  indexfi  9430  dffi3  9500  hartogslem1  9611  cantnfval2  9738  cantnfle  9740  cantnflem1  9758  tz9.1  9798  setind  9803  tcvalg  9807  frmin  9818  scott0  9955  bnd2  9962  carduni  10050  cardaleph  10158  alephinit  10164  aceq3lem  10189  dfac12lem3  10215  infmap2  10286  cflem  10314  cflemOLD  10315  cflm  10319  cflecard  10322  cfeq0  10325  cfsuc  10326  cfflb  10328  cfslb  10335  cfslb2n  10337  coftr  10342  fin23lem13  10401  fin23lem16  10404  fin23lem19  10405  fin23lem29  10410  fin1a2lem13  10481  itunitc  10490  domtriomlem  10511  axdc3lem2  10520  zorn2lem7  10571  zornn0g  10574  pwfseqlem4a  10730  pwfseqlem4  10731  wunfi  10790  wunex2  10807  wuncval  10811  rankcf  10846  tskuni  10852  axgroth6  10897  axgroth3  10900  axgroth4  10901  fzoss1  13743  fsuppmapnn0fiubex  14043  hashf1lem2  14505  cleq1lem  15031  rtrclreclem4  15110  sumeq1  15737  fsumcvg3  15777  fsum2d  15819  fsumabs  15849  fsumrlim  15859  fsumo1  15860  fsumiun  15869  prodeq1f  15954  prodeq1  15955  fprod2d  16029  lcmfunsnlem  16688  coprmprod  16708  vdwmc  17025  prmgaplem3  17100  prmgaplem4  17101  restsspw  17491  ismred2  17661  mrcval  17668  mrcuni  17679  acsfn  17717  isssc  17881  drsdirfi  18375  ipodrsima  18611  cntzssv  19368  pmtrfrn  19500  pmtrrn2  19502  pmtrdifellem1  19518  pmtrdifellem2  19519  sylow2alem2  19660  sylow2a  19661  efgval  19759  gsumzaddlem  19963  ablfac1eulem  20116  lspval  20996  lspindpi  21157  znf1o  21593  zntoslem  21598  aspval  21916  mplsubglem  22042  mpllsslem  22043  mplcoe1  22078  mplcoe5  22081  mdetunilem9  22647  uniopn  22924  fiinopn  22928  fiinbas  22980  baspartn  22982  eltg2  22986  eltg3  22990  topbas  23000  pptbas  23036  clsval  23066  neiint  23133  neips  23142  opnneissb  23143  opnssneib  23144  innei  23154  neiptoptop  23160  neiptopnei  23161  restbas  23187  restcld  23201  neitr  23209  restcls  23210  restntr  23211  cnpdis  23322  cmpsublem  23428  cmpsub  23429  fiuncmp  23433  unconn  23458  1stcfb  23474  2ndc1stc  23480  1stcrest  23482  2ndcctbss  23484  2ndcomap  23487  dis2ndc  23489  lly1stc  23525  refssex  23540  refun0  23544  llycmpkgen2  23579  txbas  23596  eltx  23597  ptuni2  23605  neitx  23636  ptpjopn  23641  ptcld  23642  txlm  23677  tx1stc  23679  txkgen  23681  xkopt  23684  xkococnlem  23688  ptcmpfi  23842  fbssfi  23866  opnfbas  23871  isfil2  23885  isfildlem  23886  snfil  23893  fsubbas  23896  ssfg  23901  fgss2  23903  fgcl  23907  fbasrn  23913  fgtr  23919  ufli  23943  uffix  23950  rnelfmlem  23981  fclscf  24054  alexsublem  24073  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  tmdgsum2  24125  subgntr  24136  opnsubg  24137  qustgpopn  24149  tsmsfbas  24157  tsmsgsum  24168  tsmsres  24173  tsmsf1o  24174  tsmsxplem1  24182  tsmsxp  24184  isust  24233  ustssel  24235  ustincl  24237  ustdiag  24238  ustinvel  24239  ustexhalf  24240  ustexsym  24245  ust0  24249  restutop  24267  ustuqtop4  24274  utopsnneiplem  24277  blssexps  24457  blssex  24458  neibl  24535  blcld  24539  met1stc  24555  met2ndci  24556  metrest  24558  prdsxmslem2  24563  metustfbas  24591  cfilucfil  24593  metuel2  24599  metustbl  24600  restmetu  24604  dscopn  24607  isngp2  24631  tgioo  24837  tgqioo  24841  zdis  24857  xrge0tsms  24875  fsumcn  24913  volivth  25661  vitalilem2  25663  itgfsum  25882  limcun  25950  recnprss  25959  dvmptfsum  26033  ftc1a  26098  plyssc  26259  efopn  26718  jensen  27050  brsslt  27848  madef  27913  tglnunirn  28574  lpvtx  29103  umgredgprv  29142  usgredgprvALT  29230  issubgr2  29307  subgrprop2  29309  egrsubgr  29312  0uhgrsubgr  29314  frcond3  30301  hhsssh  31301  shintcl  31362  chintcl  31364  spanval  31365  omlsi  31436  pjoml  31468  chnlen0  31476  chsscon3  31532  chlejb1  31544  chnle  31546  spanun  31577  h1datom  31614  cmbr4i  31633  pjoml2  31643  pjoml3  31644  lecm  31649  osumcor2i  31676  osum  31677  spansncv  31685  pjcjt2  31724  pjopyth  31752  hstel2  32251  stj  32267  stcltr1i  32306  mdi  32327  mdbr3  32329  mdbr4  32330  dmdbr  32331  dmdmd  32332  dmdbr5  32340  mdsl1i  32353  mdslmd1lem3  32359  mdslmd1lem4  32360  mdslmd1i  32361  csmdsymi  32366  atss  32378  atom1d  32385  superpos  32386  chcv1  32387  shatomici  32390  shatomistici  32393  hatomistici  32394  chrelat2  32402  chirredi  32426  atcvat4i  32429  mdsymlem2  32436  mdsymlem6  32440  dmdbr6ati  32455  dmdbr7ati  32456  xrge0tsmsd  33041  gsumle  33074  gsumvsca1  33205  gsumvsca2  33206  prmidl  33433  ismxidl  33455  zarcls1  33815  zarclsun  33816  zarclsiin  33817  zarclsint  33818  zarclssn  33819  zartop  33822  zartopon  33823  zart0  33825  zarmxt1  33826  zarcmp  33828  rhmpreimacnlem  33830  rhmpreimacn  33831  tpr2rico  33858  issiga  34076  isrnsiga  34077  sigagenval  34104  measiuns  34181  dya2icoseg  34242  dya2iocnrect  34246  dya2iocuni  34248  carsgmon  34279  carsgsigalem  34280  carsgclctunlem2  34284  carsgclctun  34286  pmeasmono  34289  pmeasadd  34290  bnj517  34861  bnj1118  34960  bnj1145  34969  bnj1154  34975  bnj1452  35028  bnj1498  35037  fineqvpow  35072  fineqvac  35073  fineqvacALT  35074  pthhashvtx  35095  kur14lem1  35174  cvmopnlem  35246  dfon2lem3  35749  dfon2lem7  35753  brsset  35853  fness  36315  fneref  36316  fnessref  36323  neibastop2lem  36326  topmeet  36330  fnejoin2  36335  tailfb  36343  filnetlem4  36347  onsucsuccmpi  36409  bj-snglss  36936  bj-elpwgALT  37020  bj-restpw  37058  bj-imdirco  37156  dissneqlem  37306  relowlssretop  37329  relowlpssretop  37330  ctbssinf  37372  pibt2  37383  matunitlindflem1  37576  ptrecube  37580  poimirlem29  37609  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  indexa  37693  indexdom  37694  neificl  37713  istotbnd3  37731  sstotbnd2  37734  sstotbnd  37735  equivtotbnd  37738  ssbnd  37748  heiborlem1  37771  heiborlem6  37776  heiborlem8  37778  heiborlem10  37780  unichnidl  37991  pridl  37997  ismaxidl  38000  igenval  38021  igenval2  38026  ispridlc  38030  relcnveq3  38277  iss2  38300  elrelscnveq3  38447  brssr  38457  lsmsat  38964  lssatomic  38967  lssats  38968  lsat0cv  38989  lcvexchlem4  38993  lcvexchlem5  38994  lsatcvatlem  39005  l1cvpat  39010  ispsubsp  39702  linepsubN  39709  pclvalN  39847  ispsubclN  39894  ispsubcl2N  39904  pclfinclN  39907  diaelrnN  41002  docavalN  41080  dochval  41308  dvh4dimat  41395  dochexmidlem1  41417  lpolconN  41444  mapdordlem2  41594  eqresfnbd  42227  ismrcd1  42654  ismrcd2  42655  ismrc  42657  mzpcompact2lem  42707  aomclem6  43016  hbtlem6  43086  rgspnval  43125  onintunirab  43188  rp-brsslt  43385  ssficl  43531  ssuncl  43532  ssdifcl  43533  sssymdifcl  43534  elmapintrab  43538  clcnvlem  43585  iunrelexpmin1  43670  iunrelexpmin2  43674  clsk3nimkb  44002  clsk1indlem1  44007  isotone1  44010  isotone2  44011  ntrclsiso  44029  gneispace  44096  gneispacess2  44108  onfrALTlem5  44513  onfrALTlem5VD  44856  islptre  45540  dvmptconst  45836  dvmptidg  45838  dvmulcncf  45846  dvdivcncf  45848  dvmptfprod  45866  stoweidlem51  45972  stoweidlem52  45973  fourierdlem103  46130  fourierdlem104  46131  ioorrnopnlem  46225  ioorrnopnxrlem  46227  salgenval  46242  ovnval2  46466  ovncvrrp  46485  ovnsubaddlem1  46491  ovnsubadd  46493  ovncvr2  46532  hspmbl  46550  elsetpreimafvssdm  47260  uhgrimisgrgriclem  47782  grimedg  47787  grtrissvtx  47795  grtrimap  47797  uspgrlimlem1  47812  uspgrlimlem2  47813  uspgrlimlem3  47814  uspgrlimlem4  47815  grlimgrtrilem1  47818  grlimgrtrilem2  47819  grlimgrtri  47820  usgrexmpl1lem  47836  usgrexmpl2lem  47841  uspgrsprfo  47871  unilbss  48549  sepfsepc  48607  unilbeu  48657  ipolubdm  48659  ipoglbdm  48662  setrec1lem1  48779  setrec1lem4  48782  setrec2fun  48784  elsetrecslem  48791  elpglem2  48804