Theorem sseq1 3965

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 3955	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3947	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3947	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	2, 3	anbiim 653	. . 3 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
5	4	ancoms 464	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
6	1, 5	sylbi 220	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ss 3925

This theorem is used by:  sseq12  3967  sseq1i  3968  sseq1d  3971  nssne2  4003  psseq1  4047  vvin  4369  uneqdifeq  4458  sbss  4486  pwjust  4568  elpwg  4570  pwpw0  4784  sssn  4797  ssunsn2  4798  unimax  4915  trss  5233  al0ssb  5276  sseliALT  5277  elssabg  5318  intabs  5324  vpwex  5353  nnullss  5448  exss  5449  releq  5768  iss  6042  relcnvtrgOLD  6274  fununi  6618  ssimaex  6973  isofrlem  7349  onssmin  7800  tfis  7860  tfisi  7864  funcnvuni  7938  ffoss  7952  f1oweALT  7978  frxp  8131  frxp2  8149  frrlem1  8292  frrlem13  8304  tfrlem1  8371  oawordeu  8549  coflton  8666  cofon1  8667  cofon2  8668  naddunif  8689  qsss  8782  boxcutc  8948  sbthlem2  9086  sbth  9095  findcard2d  9161  ssfi  9167  sbthfi  9193  php  9201  isinf  9235  unbnn2  9267  domunfican  9291  fiint  9296  finsschain  9326  indexfi  9327  dffi3  9401  hartogslem1  9514  cantnfval2  9648  cantnfle  9650  cantnflem1  9668  tz9.1  9708  tcvalg  9715  setind  9726  frmin  9731  scott0b  9876  scott0OLD  9877  bnd2  9895  carduni  9986  cardaleph  10092  alephinit  10098  aceq3lem  10123  dfac12lem3  10148  infmap2  10219  cflem  10247  cflm  10251  cflecard  10254  cfeq0  10258  cfsuc  10259  cfflb  10261  cfslb  10268  cfslb2n  10270  coftr  10275  fin23lem13  10334  fin23lem16  10337  fin23lem19  10338  fin23lem29  10343  fin1a2lem13  10414  itunitc  10423  domtriomlem  10444  axdc3lem2  10453  zorn2lem7  10504  zornn0g  10507  pwfseqlem4a  10664  pwfseqlem4  10665  wunfi  10724  wunex2  10741  wuncval  10745  rankcf  10780  tskuni  10786  axgroth6  10831  axgroth3  10834  axgroth4  10835  fzoss1  13734  fsuppmapnn0fiubex  14048  hashf1lem2  14513  cleq1lem  15045  rtrclreclem4  15124  sumeq1  15766  fsumcvg3  15806  fsum2d  15848  fsumabs  15879  fsumrlim  15889  fsumo1  15890  fsumiun  15899  prodeq1f  15986  prodeq1  15987  fprod2d  16061  lcmfunsnlem  16724  coprmprod  16744  vdwmc  17063  prmgaplem3  17138  prmgaplem4  17139  restsspw  17509  ismred2  17680  mrcval  17691  mrcuni  17702  acsfn  17740  isssc  17902  drsdirfi  18386  ipodrsima  18622  cntzssv  19429  pmtrfrn  19559  pmtrrn2  19561  pmtrdifellem1  19577  pmtrdifellem2  19578  sylow2alem2  19719  sylow2a  19720  efgval  19818  gsumzaddlem  20022  ablfac1eulem  20175  gsumle  20246  rgspnval  20748  lspval  21133  lspindpi  21293  unichnlidl  21399  rspprop  21407  prmidl  21502  znf1o  21738  zntoslem  21743  aspval  22059  mplsubglem  22185  mpllsslem  22186  mplcoe1  22225  mplcoe5  22228  mdetunilem9  22814  uniopn  23091  fiinopn  23095  fiinbas  23146  baspartn  23148  eltg2  23152  eltg3  23156  topbas  23166  pptbas  23202  clsval  23231  neiint  23298  neips  23307  opnneissb  23308  opnssneib  23309  innei  23319  neiptoptop  23325  neiptopnei  23326  restbas  23352  restcld  23366  neitr  23374  restcls  23375  restntr  23376  cnpdis  23487  cmpsublem  23593  cmpsub  23594  fiuncmp  23598  unconn  23623  1stcfb  23639  2ndc1stc  23645  1stcrest  23647  2ndcctbss  23649  2ndcomap  23652  dis2ndc  23654  lly1stc  23690  refssex  23705  refun0  23709  llycmpkgen2  23744  txbas  23761  eltx  23762  ptuni2  23770  neitx  23801  ptpjopn  23806  ptcld  23807  txlm  23842  tx1stc  23844  txkgen  23846  xkopt  23849  xkococnlem  23853  ptcmpfi  24007  fbssfi  24031  opnfbas  24036  isfil2  24050  isfildlem  24051  snfil  24058  fsubbas  24061  ssfg  24066  fgss2  24068  fgcl  24072  fbasrn  24078  fgtr  24084  ufli  24108  uffix  24115  rnelfmlem  24146  fclscf  24219  alexsublem  24238  alexsubALTlem2  24242  alexsubALTlem3  24243  alexsubALTlem4  24244  alexsubALT  24245  tmdgsum2  24290  subgntr  24301  opnsubg  24302  qustgpopn  24314  tsmsfbas  24322  tsmsgsum  24333  tsmsres  24338  tsmsf1o  24339  tsmsxplem1  24347  tsmsxp  24349  isust  24398  ustssel  24400  ustincl  24402  ustdiag  24403  ustinvel  24404  ustexhalf  24405  ustexsym  24410  ust0  24414  restutop  24431  ustuqtop4  24438  utopsnneiplem  24441  blssexps  24620  blssex  24621  neibl  24695  blcld  24699  met1stc  24715  met2ndci  24716  metrest  24718  prdsxmslem2  24723  metustfbas  24751  cfilucfil  24753  metuel2  24759  metustbl  24760  restmetu  24764  dscopn  24767  isngp2  24791  tgioo  24990  tgqioo  24994  zdis  25011  xrge0tsms  25029  fsumcn  25066  volivth  25803  vitalilem2  25805  itgfsum  26023  limcun  26091  recnprss  26100  dvmptfsum  26171  ftc1a  26233  plyssc  26394  efopn  26860  jensen  27190  brslts  27992  madef  28066  tglnunirn  28854  brprlng  29225  lpvtx  29455  umgredgprv  29494  usgredgprvALT  29582  issubgr2  29659  subgrprop2  29661  egrsubgr  29664  0uhgrsubgr  29666  frcond3  30657  hhsssh  31658  shintcl  31719  chintcl  31721  spanval  31722  omlsi  31793  pjoml  31825  chnlen0  31833  chsscon3  31889  chlejb1  31901  chnle  31903  spanun  31934  h1datom  31971  cmbr4i  31990  pjoml2  32000  pjoml3  32001  lecm  32006  osumcor2i  32033  osum  32034  spansncv  32042  pjcjt2  32081  pjopyth  32109  hstel2  32608  stj  32624  stcltr1i  32663  mdi  32684  mdbr3  32686  mdbr4  32687  dmdbr  32688  dmdmd  32689  dmdbr5  32697  mdsl1i  32710  mdslmd1lem3  32716  mdslmd1lem4  32717  mdslmd1i  32718  csmdsymi  32723  atss  32735  atom1d  32742  superpos  32743  chcv1  32744  shatomici  32747  shatomistici  32750  hatomistici  32751  chrelat2  32759  chirredi  32783  atcvat4i  32786  mdsymlem2  32793  mdsymlem6  32797  dmdbr6ati  32812  dmdbr7ati  32813  xrge0tsmsd  33424  gsumvsca1  33577  gsumvsca2  33578  ismxidl  33776  constrfiss  34172  zarcls1  34290  zarclsun  34291  zarclsiin  34292  zarclsint  34293  zarclssn  34294  zartop  34297  zartopon  34298  zart0  34300  zarmxt1  34301  zarcmp  34303  rhmpreimacnlem  34305  rhmpreimacn  34306  tpr2rico  34333  issiga  34533  isrnsiga  34534  sigagenval  34562  measiuns  34639  dya2icoseg  34699  dya2iocnrect  34703  dya2iocuni  34705  carsgmon  34736  carsgsigalem  34737  carsgclctunlem2  34741  carsgclctun  34743  pmeasmono  34746  pmeasadd  34747  bnj517  35305  bnj1118  35404  bnj1145  35413  bnj1154  35419  bnj1452  35472  bnj1498  35481  rankscottu  35547  fineqvpow  35552  fineqvac  35553  fineqvacALT  35554  setindregs  35567  tz9.1regs  35571  fineqvr1ombregs  35575  rankkardu  35608  vonf1wev  35616  vonf1owevOLD  35618  pthhashvtx  35641  kur14lem1  35719  cvmopnlem  35791  dfon2lem3  36296  dfon2lem7  36300  brsset  36400  fness  36901  fneref  36902  fnessref  36909  neibastop2lem  36912  topmeet  36916  fnejoin2  36921  tailfb  36929  filnetlem4  36933  onsucsuccmpi  36995  ttcwf2  37077  ttcexg  37084  bj-snglss  37647  bj-elpwgALT  37731  bj-restpw  37775  bj-imdirco  37875  dissneqlem  38027  relowlssretop  38050  relowlpssretop  38051  ctbssinf  38093  pibt2  38104  matunitlindflem1  38308  ptrecube  38312  poimirlem29  38341  mblfinlem2  38350  mblfinlem3  38351  mblfinlem4  38352  ismblfin  38353  ovoliunnfl  38354  voliunnfl  38356  volsupnfl  38357  indexa  38425  indexdom  38426  neificl  38445  istotbnd3  38463  sstotbnd2  38466  sstotbnd  38467  equivtotbnd  38470  ssbnd  38480  heiborlem1  38503  heiborlem6  38508  heiborlem8  38510  heiborlem10  38512  unichnidl  38723  pridl  38729  ismaxidl  38732  igenval  38753  igenval2  38758  ispridlc  38762  relcnveq3  39017  iss2  39034  brssr  39271  elrelscnveq3  39317  lsmsat  39823  lssatomic  39826  lssats  39827  lsat0cv  39848  lcvexchlem4  39852  lcvexchlem5  39853  lsatcvatlem  39864  l1cvpat  39869  ispsubsp  40560  linepsubN  40567  pclvalN  40705  ispsubclN  40752  ispsubcl2N  40762  pclfinclN  40765  diaelrnN  41860  docavalN  41938  dochval  42166  dvh4dimat  42253  dochexmidlem1  42275  lpolconN  42302  mapdordlem2  42452  eqresfnbd  43044  ismrcd1  43470  ismrcd2  43471  ismrc  43473  mzpcompact2lem  43523  aomclem6  43827  hbtlem6  43897  onintunirab  43995  rp-brsslt  44190  ssficl  44336  ssuncl  44337  ssdifcl  44338  sssymdifcl  44339  elmapintrab  44343  clcnvlem  44390  iunrelexpmin1  44475  iunrelexpmin2  44479  clsk3nimkb  44807  clsk1indlem1  44812  isotone1  44815  isotone2  44816  ntrclsiso  44834  gneispace  44901  gneispacess2  44913  onfrALTlem5  45292  onfrALTlem5VD  45634  relpfrlem  45703  modelaxreplem1  45728  islptre  46376  dvmptconst  46670  dvmptidg  46672  dvmulcncf  46680  dvdivcncf  46682  dvmptfprod  46700  stoweidlem51  46806  stoweidlem52  46807  fourierdlem103  46964  fourierdlem104  46965  ioorrnopnlem  47059  ioorrnopnxrlem  47061  salgenval  47076  ovnval2  47300  ovncvrrp  47319  ovnsubaddlem1  47325  ovnsubadd  47327  ovncvr2  47366  hspmbl  47384  elsetpreimafvssdm  48176  isubgredg  48672  uhgrimisgrgriclem  48736  grimedg  48741  grtrissvtx  48750  grtrimap  48754  stgredgiun  48764  isubgr3stgrlem6  48777  isubgr3stgrlem7  48778  uspgrlimlem1  48794  uspgrlimlem2  48795  uspgrlimlem3  48796  uspgrlimlem4  48797  clnbgrvtxedg  48800  grlimedgclnbgr  48801  grlimpredg  48804  grlimprclnbgrvtx  48805  grlimgredgex  48806  grlimgrtrilem1  48807  grlimgrtrilem2  48808  grlimgrtri  48809  usgrexmpl1lem  48827  usgrexmpl2lem  48832  uspgrsprfo  48954  unilbss  49637  sepfsepc  49747  unilbeu  49804  ipolubdm  49806  ipoglbdm  49809  discsubc  49883  iinfconstbas  49885  setrec1lem1  50506  setrec1lem4  50509  setrec2fun  50511  elsetrecslem  50518  elpglem2  50531