Theorem sseq1 3963

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 3953	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3944	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3944	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	2, 3	anbiim 641	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
5	4	ancoms 458	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
6	1, 5	sylbi 217	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  sseq12  3965  sseq1i  3966  sseq1d  3969  nssne2  4001  psseq1  4043  uneqdifeq  4446  sbss  4472  pwjust  4554  elpwg  4556  pwpw0  4767  sssn  4780  ssunsn2  4781  unimax  4897  trss  5212  al0ssb  5250  sseliALT  5251  elssabg  5285  intabs  5291  vpwex  5319  nnullss  5409  exss  5410  releq  5724  iss  5990  relcnvtrg  6219  fununi  6561  ssimaex  6912  isofrlem  7281  onssmin  7732  tfis  7795  tfisi  7799  funcnvuni  7872  ffoss  7888  f1oweALT  7914  frxp  8066  frxp2  8084  frrlem1  8226  frrlem13  8238  tfrlem1  8305  oawordeu  8480  coflton  8596  cofon1  8597  cofon2  8598  naddunif  8618  qsss  8710  boxcutc  8875  sbthlem2  9012  sbth  9021  findcard2d  9090  ssfi  9097  sbthfi  9123  php  9131  isinf  9165  isinfOLD  9166  unbnn2  9202  domunfican  9230  fiint  9235  fiintOLD  9236  finsschain  9268  indexfi  9269  dffi3  9340  hartogslem1  9453  cantnfval2  9584  cantnfle  9586  cantnflem1  9604  tz9.1  9644  setind  9649  tcvalg  9653  frmin  9664  scott0  9801  bnd2  9808  carduni  9896  cardaleph  10002  alephinit  10008  aceq3lem  10033  dfac12lem3  10059  infmap2  10130  cflem  10158  cflemOLD  10159  cflm  10163  cflecard  10166  cfeq0  10169  cfsuc  10170  cfflb  10172  cfslb  10179  cfslb2n  10181  coftr  10186  fin23lem13  10245  fin23lem16  10248  fin23lem19  10249  fin23lem29  10254  fin1a2lem13  10325  itunitc  10334  domtriomlem  10355  axdc3lem2  10364  zorn2lem7  10415  zornn0g  10418  pwfseqlem4a  10574  pwfseqlem4  10575  wunfi  10634  wunex2  10651  wuncval  10655  rankcf  10690  tskuni  10696  axgroth6  10741  axgroth3  10744  axgroth4  10745  fzoss1  13607  fsuppmapnn0fiubex  13917  hashf1lem2  14381  cleq1lem  14907  rtrclreclem4  14986  sumeq1  15614  fsumcvg3  15654  fsum2d  15696  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fsumiun  15746  prodeq1f  15831  prodeq1  15832  fprod2d  15906  lcmfunsnlem  16570  coprmprod  16590  vdwmc  16908  prmgaplem3  16983  prmgaplem4  16984  restsspw  17353  ismred2  17523  mrcval  17534  mrcuni  17545  acsfn  17583  isssc  17745  drsdirfi  18229  ipodrsima  18465  cntzssv  19225  pmtrfrn  19355  pmtrrn2  19357  pmtrdifellem1  19373  pmtrdifellem2  19374  sylow2alem2  19515  sylow2a  19516  efgval  19614  gsumzaddlem  19818  ablfac1eulem  19971  gsumle  20042  rgspnval  20515  lspval  20896  lspindpi  21057  znf1o  21476  zntoslem  21481  aspval  21798  mplsubglem  21924  mpllsslem  21925  mplcoe1  21960  mplcoe5  21963  mdetunilem9  22523  uniopn  22800  fiinopn  22804  fiinbas  22855  baspartn  22857  eltg2  22861  eltg3  22865  topbas  22875  pptbas  22911  clsval  22940  neiint  23007  neips  23016  opnneissb  23017  opnssneib  23018  innei  23028  neiptoptop  23034  neiptopnei  23035  restbas  23061  restcld  23075  neitr  23083  restcls  23084  restntr  23085  cnpdis  23196  cmpsublem  23302  cmpsub  23303  fiuncmp  23307  unconn  23332  1stcfb  23348  2ndc1stc  23354  1stcrest  23356  2ndcctbss  23358  2ndcomap  23361  dis2ndc  23363  lly1stc  23399  refssex  23414  refun0  23418  llycmpkgen2  23453  txbas  23470  eltx  23471  ptuni2  23479  neitx  23510  ptpjopn  23515  ptcld  23516  txlm  23551  tx1stc  23553  txkgen  23555  xkopt  23558  xkococnlem  23562  ptcmpfi  23716  fbssfi  23740  opnfbas  23745  isfil2  23759  isfildlem  23760  snfil  23767  fsubbas  23770  ssfg  23775  fgss2  23777  fgcl  23781  fbasrn  23787  fgtr  23793  ufli  23817  uffix  23824  rnelfmlem  23855  fclscf  23928  alexsublem  23947  alexsubALTlem2  23951  alexsubALTlem3  23952  alexsubALTlem4  23953  alexsubALT  23954  tmdgsum2  23999  subgntr  24010  opnsubg  24011  qustgpopn  24023  tsmsfbas  24031  tsmsgsum  24042  tsmsres  24047  tsmsf1o  24048  tsmsxplem1  24056  tsmsxp  24058  isust  24107  ustssel  24109  ustincl  24111  ustdiag  24112  ustinvel  24113  ustexhalf  24114  ustexsym  24119  ust0  24123  restutop  24141  ustuqtop4  24148  utopsnneiplem  24151  blssexps  24330  blssex  24331  neibl  24405  blcld  24409  met1stc  24425  met2ndci  24426  metrest  24428  prdsxmslem2  24433  metustfbas  24461  cfilucfil  24463  metuel2  24469  metustbl  24470  restmetu  24474  dscopn  24477  isngp2  24501  tgioo  24700  tgqioo  24704  zdis  24721  xrge0tsms  24739  fsumcn  24777  volivth  25524  vitalilem2  25526  itgfsum  25744  limcun  25812  recnprss  25821  dvmptfsum  25895  ftc1a  25960  plyssc  26121  efopn  26583  jensen  26915  brsslt  27714  madef  27784  tglnunirn  28511  lpvtx  29031  umgredgprv  29070  usgredgprvALT  29158  issubgr2  29235  subgrprop2  29237  egrsubgr  29240  0uhgrsubgr  29242  frcond3  30231  hhsssh  31231  shintcl  31292  chintcl  31294  spanval  31295  omlsi  31366  pjoml  31398  chnlen0  31406  chsscon3  31462  chlejb1  31474  chnle  31476  spanun  31507  h1datom  31544  cmbr4i  31563  pjoml2  31573  pjoml3  31574  lecm  31579  osumcor2i  31606  osum  31607  spansncv  31615  pjcjt2  31654  pjopyth  31682  hstel2  32181  stj  32197  stcltr1i  32236  mdi  32257  mdbr3  32259  mdbr4  32260  dmdbr  32261  dmdmd  32262  dmdbr5  32270  mdsl1i  32283  mdslmd1lem3  32289  mdslmd1lem4  32290  mdslmd1i  32291  csmdsymi  32296  atss  32308  atom1d  32315  superpos  32316  chcv1  32317  shatomici  32320  shatomistici  32323  hatomistici  32324  chrelat2  32332  chirredi  32356  atcvat4i  32359  mdsymlem2  32366  mdsymlem6  32370  dmdbr6ati  32385  dmdbr7ati  32386  xrge0tsmsd  33028  gsumvsca1  33178  gsumvsca2  33179  prmidl  33387  ismxidl  33409  constrfiss  33717  zarcls1  33835  zarclsun  33836  zarclsiin  33837  zarclsint  33838  zarclssn  33839  zartop  33842  zartopon  33843  zart0  33845  zarmxt1  33846  zarcmp  33848  rhmpreimacnlem  33850  rhmpreimacn  33851  tpr2rico  33878  issiga  34078  isrnsiga  34079  sigagenval  34106  measiuns  34183  dya2icoseg  34244  dya2iocnrect  34248  dya2iocuni  34250  carsgmon  34281  carsgsigalem  34282  carsgclctunlem2  34286  carsgclctun  34288  pmeasmono  34291  pmeasadd  34292  bnj517  34851  bnj1118  34950  bnj1145  34959  bnj1154  34965  bnj1452  35018  bnj1498  35027  setindregs  35064  tz9.1regs  35066  fineqvpow  35070  fineqvac  35071  fineqvacALT  35072  vonf1owev  35080  pthhashvtx  35100  kur14lem1  35178  cvmopnlem  35250  dfon2lem3  35758  dfon2lem7  35762  brsset  35862  fness  36322  fneref  36323  fnessref  36330  neibastop2lem  36333  topmeet  36337  fnejoin2  36342  tailfb  36350  filnetlem4  36354  onsucsuccmpi  36416  bj-snglss  36943  bj-elpwgALT  37027  bj-restpw  37065  bj-imdirco  37163  dissneqlem  37313  relowlssretop  37336  relowlpssretop  37337  ctbssinf  37379  pibt2  37390  matunitlindflem1  37595  ptrecube  37599  poimirlem29  37628  mblfinlem2  37637  mblfinlem3  37638  mblfinlem4  37639  ismblfin  37640  ovoliunnfl  37641  voliunnfl  37643  volsupnfl  37644  indexa  37712  indexdom  37713  neificl  37732  istotbnd3  37750  sstotbnd2  37753  sstotbnd  37754  equivtotbnd  37757  ssbnd  37767  heiborlem1  37790  heiborlem6  37795  heiborlem8  37797  heiborlem10  37799  unichnidl  38010  pridl  38016  ismaxidl  38019  igenval  38040  igenval2  38045  ispridlc  38049  relcnveq3  38294  iss2  38311  elrelscnveq3  38467  brssr  38477  lsmsat  38986  lssatomic  38989  lssats  38990  lsat0cv  39011  lcvexchlem4  39015  lcvexchlem5  39016  lsatcvatlem  39027  l1cvpat  39032  ispsubsp  39724  linepsubN  39731  pclvalN  39869  ispsubclN  39916  ispsubcl2N  39926  pclfinclN  39929  diaelrnN  41024  docavalN  41102  dochval  41330  dvh4dimat  41417  dochexmidlem1  41439  lpolconN  41466  mapdordlem2  41616  eqresfnbd  42205  ismrcd1  42671  ismrcd2  42672  ismrc  42674  mzpcompact2lem  42724  aomclem6  43032  hbtlem6  43102  onintunirab  43200  rp-brsslt  43396  ssficl  43542  ssuncl  43543  ssdifcl  43544  sssymdifcl  43545  elmapintrab  43549  clcnvlem  43596  iunrelexpmin1  43681  iunrelexpmin2  43685  clsk3nimkb  44013  clsk1indlem1  44018  isotone1  44021  isotone2  44022  ntrclsiso  44040  gneispace  44107  gneispacess2  44119  onfrALTlem5  44516  onfrALTlem5VD  44858  relpfrlem  44927  modelaxreplem1  44952  islptre  45601  dvmptconst  45897  dvmptidg  45899  dvmulcncf  45907  dvdivcncf  45909  dvmptfprod  45927  stoweidlem51  46033  stoweidlem52  46034  fourierdlem103  46191  fourierdlem104  46192  ioorrnopnlem  46286  ioorrnopnxrlem  46288  salgenval  46303  ovnval2  46527  ovncvrrp  46546  ovnsubaddlem1  46552  ovnsubadd  46554  ovncvr2  46593  hspmbl  46611  elsetpreimafvssdm  47371  isubgredg  47851  uhgrimisgrgriclem  47915  grimedg  47920  grtrissvtx  47929  grtrimap  47933  stgredgiun  47943  isubgr3stgrlem6  47956  isubgr3stgrlem7  47957  uspgrlimlem1  47973  uspgrlimlem2  47974  uspgrlimlem3  47975  uspgrlimlem4  47976  clnbgrvtxedg  47979  grlimedgclnbgr  47980  grlimpredg  47983  grlimprclnbgrvtx  47984  grlimgredgex  47985  grlimgrtrilem1  47986  grlimgrtrilem2  47987  grlimgrtri  47988  usgrexmpl1lem  48006  usgrexmpl2lem  48011  uspgrsprfo  48133  unilbss  48803  sepfsepc  48913  unilbeu  48970  ipolubdm  48972  ipoglbdm  48975  discsubc  49050  iinfconstbas  49052  setrec1lem1  49673  setrec1lem4  49676  setrec2fun  49678  elsetrecslem  49685  elpglem2  49698