Theorem sseq1 3959

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 3949	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3941	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3		sstr2 3941	. . . 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 3902

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 2155  ax-ext 2734

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

This theorem is used by:  sseq12  3961  sseq1i  3962  sseq1d  3965  nssne2  3997  psseq1  4041  vvin  4362  uneqdifeq  4451  sbss  4479  pwjust  4561  elpwg  4563  pwpw0  4777  sssn  4790  ssunsn2  4791  unimax  4908  trss  5226  al0ssb  5269  sseliALT  5270  elssabg  5311  intabs  5317  vpwex  5346  nnullss  5441  exss  5442  releq  5761  iss  6035  relcnvtrgOLD  6268  fununi  6612  ssimaex  6967  isofrlem  7345  onssmin  7795  tfis  7855  tfisi  7859  funcnvuni  7933  ffoss  7947  f1oweALT  7973  frxp  8128  frxp2  8146  frrlem1  8289  frrlem13  8301  tfrlem1  8368  oawordeu  8546  coflton  8663  cofon1  8664  cofon2  8665  naddunif  8686  qsss  8779  boxcutc  8952  sbthlem2  9090  sbth  9099  findcard2d  9165  ssfi  9171  sbthfi  9197  php  9205  isinf  9239  unbnn2  9271  domunfican  9295  fiint  9300  finsschain  9330  indexfi  9331  dffi3  9405  hartogslem1  9518  cantnfval2  9652  cantnfle  9654  cantnflem1  9672  tz9.1  9712  tcvalg  9719  setind  9730  frmin  9735  scott0b  9880  scott0OLD  9881  bnd2  9899  carduni  9990  cardaleph  10096  alephinit  10102  aceq3lem  10127  dfac12lem3  10152  infmap2  10223  cflem  10251  cflm  10255  cflecard  10258  cfeq0  10262  cfsuc  10263  cfflb  10265  cfslb  10272  cfslb2n  10274  coftr  10279  fin23lem13  10338  fin23lem16  10341  fin23lem19  10342  fin23lem29  10347  fin1a2lem13  10418  itunitc  10427  domtriomlem  10448  axdc3lem2  10457  zorn2lem7  10508  zornn0g  10511  pwfseqlem4a  10674  pwfseqlem4  10675  wunfi  10734  wunex2  10751  wuncval  10755  rankcf  10790  tskuni  10796  axgroth6  10841  axgroth3  10844  axgroth4  10845  fzoss1  13746  fsuppmapnn0fiubex  14060  hashf1lem2  14525  cleq1lem  15059  rtrclreclem4  15138  sumeq1  15780  fsumcvg3  15819  fsum2d  15861  fsumabs  15892  fsumrlim  15902  fsumo1  15903  fsumiun  15912  prodeq1f  15999  prodeq1  16000  fprod2d  16074  lcmfunsnlem  16737  coprmprod  16757  vdwmc  17076  prmgaplem3  17151  prmgaplem4  17152  restsspw  17522  ismred2  17693  mrcval  17704  mrcuni  17715  acsfn  17753  isssc  17915  drsdirfi  18399  ipodrsima  18635  cntzssv  19461  pmtrfrn  19591  pmtrrn2  19593  pmtrdifellem1  19609  pmtrdifellem2  19610  sylow2alem2  19751  sylow2a  19752  efgval  19850  gsumzaddlem  20054  ablfac1eulem  20207  gsumle  20278  rgspnval  20780  lspval  21165  lspindpi  21325  unichnlidl  21431  rspprop  21439  prmidl  21534  znf1o  21770  zntoslem  21775  aspval  22093  mplsubglem  22219  mpllsslem  22220  mplcoe1  22259  mplcoe5  22262  mdetunilem9  22848  matunitlindflem1  22907  uniopn  23128  fiinopn  23132  fiinbas  23183  baspartn  23185  eltg2  23189  eltg3  23193  topbas  23203  pptbas  23239  clsval  23268  neiint  23335  neips  23344  opnneissb  23345  opnssneib  23346  innei  23356  neiptoptop  23362  neiptopnei  23363  restbas  23389  restcld  23403  neitr  23411  restcls  23412  restntr  23413  cnpdis  23524  cmpsublem  23630  cmpsub  23631  fiuncmp  23635  unconn  23660  1stcfb  23676  2ndc1stc  23682  1stcrest  23684  2ndcctbss  23687  2ndcomap  23690  dis2ndc  23692  lly1stc  23728  refssex  23743  refun0  23747  llycmpkgen2  23782  txbas  23799  eltx  23800  ptuni2  23808  neitx  23839  ptpjopn  23844  ptcld  23845  txlm  23880  tx1stc  23882  txkgen  23884  xkopt  23887  xkococnlem  23891  ptcmpfi  24045  fbssfi  24069  opnfbas  24074  isfil2  24088  isfildlem  24089  snfil  24096  fsubbas  24099  ssfg  24104  fgss2  24106  fgcl  24110  fbasrn  24116  fgtr  24122  ufli  24146  uffix  24153  rnelfmlem  24184  fclscf  24257  alexsublem  24276  alexsubALTlem2  24280  alexsubALTlem3  24281  alexsubALTlem4  24282  alexsubALT  24283  tmdgsum2  24328  subgntr  24339  opnsubg  24340  qustgpopn  24352  tsmsfbas  24360  tsmsgsum  24371  tsmsres  24376  tsmsf1o  24377  tsmsxplem1  24385  tsmsxp  24387  isust  24436  ustssel  24438  ustincl  24440  ustdiag  24441  ustinvel  24442  ustexhalf  24443  ustexsym  24448  ust0  24452  restutop  24469  ustuqtop4  24476  utopsnneiplem  24479  blssexps  24658  blssex  24659  neibl  24733  blcld  24737  met1stc  24753  met2ndci  24754  metrest  24756  prdsxmslem2  24761  metustfbas  24789  cfilucfil  24791  metuel2  24797  metustbl  24798  restmetu  24802  dscopn  24805  isngp2  24829  tgioo  25028  tgqioo  25032  zdis  25049  xrge0tsms  25067  fsumcn  25104  volivth  25841  vitalilem2  25843  itgfsum  26061  limcun  26129  recnprss  26138  dvmptfsum  26209  ftc1a  26271  plyssc  26432  efopn  26903  jensen  27233  brslts  28035  madef  28109  tglnunirn  28898  brprlng  29303  lpvtx  29533  umgredgprv  29572  usgredgprvALT  29663  issubgr2  29740  subgrprop2  29742  egrsubgr  29745  0uhgrsubgr  29747  pthhashvtx  30202  frcond3  30757  hhsssh  31758  shintcl  31819  chintcl  31821  spanval  31822  omlsi  31893  pjoml  31925  chnlen0  31933  chsscon3  31989  chlejb1  32001  chnle  32003  spanun  32034  h1datom  32071  cmbr4i  32090  pjoml2  32100  pjoml3  32101  lecm  32106  osumcor2i  32133  osum  32134  spansncv  32142  pjcjt2  32181  pjopyth  32209  hstel2  32708  stj  32724  stcltr1i  32763  mdi  32784  mdbr3  32786  mdbr4  32787  dmdbr  32788  dmdmd  32789  dmdbr5  32797  mdsl1i  32810  mdslmd1lem3  32816  mdslmd1lem4  32817  mdslmd1i  32818  csmdsymi  32823  atss  32835  atom1d  32842  superpos  32843  chcv1  32844  shatomici  32847  shatomistici  32850  hatomistici  32851  chrelat2  32859  chirredi  32883  atcvat4i  32886  mdsymlem2  32893  mdsymlem6  32897  dmdbr6ati  32912  dmdbr7ati  32913  xrge0tsmsd  33521  gsumvsca1  33674  gsumvsca2  33675  ismxidl  33873  constrfiss  34269  zarcls1  34387  zarclsun  34388  zarclsiin  34389  zarclsint  34390  zarclssn  34391  zartop  34394  zartopon  34395  zart0  34397  zarmxt1  34398  zarcmp  34400  rhmpreimacnlem  34402  rhmpreimacn  34403  tpr2rico  34430  issiga  34630  isrnsiga  34631  sigagenval  34659  measiuns  34736  dya2icoseg  34796  dya2iocnrect  34800  dya2iocuni  34802  carsgmon  34833  carsgsigalem  34834  carsgclctunlem2  34838  carsgclctun  34840  pmeasmono  34843  pmeasadd  34844  bnj517  35402  bnj1118  35501  bnj1145  35510  bnj1154  35516  bnj1452  35569  bnj1498  35578  rankscottu  35644  fineqvpow  35649  fineqvac  35650  fineqvacALT  35651  setindregs  35664  tz9.1regs  35668  fineqvr1ombregs  35672  rankkardu  35705  vonf1wev  35713  vonf1owevOLD  35715  kur14lem1  35793  cvmopnlem  35865  dfon2lem3  36370  dfon2lem7  36374  brsset  36474  fness  36976  fneref  36977  fnessref  36984  neibastop2lem  36987  topmeet  36991  fnejoin2  36996  tailfb  37004  filnetlem4  37008  onsucsuccmpi  37070  ttcwf2  37152  ttcexg  37159  bj-snglss  37722  bj-elpwgALT  37806  bj-restpw  37850  bj-imdirco  37950  dissneqlem  38102  relowlssretop  38125  relowlpssretop  38126  ctbssinf  38168  pibt2  38179  ptrecube  38377  poimirlem29  38406  mblfinlem2  38415  mblfinlem3  38416  mblfinlem4  38417  ismblfin  38418  ovoliunnfl  38419  voliunnfl  38421  volsupnfl  38422  indexa  38491  indexdom  38492  neificl  38511  istotbnd3  38529  sstotbnd2  38532  sstotbnd  38533  equivtotbnd  38536  ssbnd  38546  heiborlem1  38569  heiborlem6  38574  heiborlem8  38576  heiborlem10  38578  unichnidl  38789  pridl  38795  ismaxidl  38798  igenval  38819  igenval2  38824  ispridlc  38828  relcnveq3  39083  iss2  39100  brssr  39337  elrelscnveq3  39383  lsmsat  39889  lssatomic  39892  lssats  39893  lsat0cv  39914  lcvexchlem4  39918  lcvexchlem5  39919  lsatcvatlem  39930  l1cvpat  39935  ispsubsp  40626  linepsubN  40633  pclvalN  40771  ispsubclN  40818  ispsubcl2N  40828  pclfinclN  40831  diaelrnN  41926  docavalN  42004  dochval  42232  dvh4dimat  42319  dochexmidlem1  42341  lpolconN  42368  mapdordlem2  42518  eqresfnbd  43110  ismrcd1  43551  ismrcd2  43552  ismrc  43554  mzpcompact2lem  43604  aomclem6  43908  hbtlem6  43978  onintunirab  44076  rp-brsslt  44271  ssficl  44417  ssuncl  44418  ssdifcl  44419  sssymdifcl  44420  elmapintrab  44424  clcnvlem  44471  iunrelexpmin1  44556  iunrelexpmin2  44560  clsk3nimkb  44888  clsk1indlem1  44893  isotone1  44896  isotone2  44897  ntrclsiso  44915  gneispace  44982  gneispacess2  44994  onfrALTlem5  45373  onfrALTlem5VD  45715  relpfrlem  45784  modelaxreplem1  45809  islptre  46457  dvmptconst  46751  dvmptidg  46753  dvmulcncf  46761  dvdivcncf  46763  dvmptfprod  46781  stoweidlem51  46887  stoweidlem52  46888  fourierdlem103  47045  fourierdlem104  47046  ioorrnopnlem  47140  ioorrnopnxrlem  47142  salgenval  47157  ovnval2  47381  ovncvrrp  47400  ovnsubaddlem1  47406  ovnsubadd  47408  ovncvr2  47447  hspmbl  47465  elsetpreimafvssdm  48294  isubgredg  48790  uhgrimisgrgriclem  48854  grimedg  48859  grtrissvtx  48868  grtrimap  48872  stgredgiun  48882  isubgr3stgrlem6  48895  isubgr3stgrlem7  48896  uspgrlimlem1  48912  uspgrlimlem2  48913  uspgrlimlem3  48914  uspgrlimlem4  48915  clnbgrvtxedg  48918  grlimedgclnbgr  48919  grlimpredg  48922  grlimprclnbgrvtx  48923  grlimgredgex  48924  grlimgrtrilem1  48925  grlimgrtrilem2  48926  grlimgrtri  48927  usgrexmpl1lem  48945  usgrexmpl2lem  48950  uspgrsprfo  49072  unilbss  49754  sepfsepc  49862  unilbeu  49919  ipolubdm  49921  ipoglbdm  49924  discsubc  49998  iinfconstbas  50000  setrec1lem1  50621  setrec1lem4  50624  setrec2fun  50626  elsetrecslem  50633  elpglem2  50646