Theorem sseq1 3940

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 3930	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3922	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 485	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3922	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
5	4	adantr 484	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
6	3, 5	impbid 215	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
7	1, 6	sylbi 220	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  sseq12  3942  sseq1i  3943  sseq1d  3946  nssne2  3976  psseq1  4015  uneqdifeq  4396  sbss  4420  pwjust  4498  elpwg  4500  elpwOLD  4503  elpwgOLD  4504  pwpw0  4706  sssn  4719  ssunsn2  4720  pwsnOLD  4793  unimax  4836  trss  5145  al0ssb  5176  sseliALT  5177  elssabg  5203  intabs  5209  nnullss  5319  exss  5320  fri  5481  releq  5615  iss  5870  relcnvtrg  6086  fununi  6399  ssimaex  6723  isofrlem  7072  onssmin  7492  tfis  7549  tfisi  7553  funcnvuni  7618  ffoss  7629  f1oweALT  7655  frxp  7803  wfrlem1  7937  wfrlem4  7941  wfrlem15  7952  tfrlem1  7995  oawordeu  8164  qsss  8341  boxcutc  8488  sbthlem2  8612  sbth  8621  php  8685  isinf  8715  findcard2d  8744  unbnn2  8759  domunfican  8775  fiint  8779  finsschain  8815  indexfi  8816  dffi3  8879  hartogslem1  8990  cantnfval2  9116  cantnfle  9118  cantnflem1  9136  tz9.1  9155  setind  9160  tcvalg  9164  scott0  9299  bnd2  9306  carduni  9394  cardaleph  9500  alephinit  9506  aceq3lem  9531  dfac12lem3  9556  infmap2  9629  cflem  9657  cflm  9661  cflecard  9664  cfeq0  9667  cfsuc  9668  cfflb  9670  cfslb  9677  cfslb2n  9679  coftr  9684  fin23lem13  9743  fin23lem16  9746  fin23lem19  9747  fin23lem29  9752  fin1a2lem13  9823  itunitc  9832  domtriomlem  9853  axdc3lem2  9862  zorn2lem7  9913  zornn0g  9916  fpwwe2lem5  10045  pwfseqlem4a  10072  pwfseqlem4  10073  wunfi  10132  wunex2  10149  wuncval  10153  rankcf  10188  tskuni  10194  axgroth6  10239  axgroth3  10242  axgroth4  10243  fzoss1  13059  fsuppmapnn0fiubex  13355  hashf1lem2  13810  cleq1lem  14333  rtrclreclem4  14412  sumeq1  15037  fsumcvg3  15078  fsum2d  15118  fsumabs  15148  fsumrlim  15158  fsumo1  15159  fsumiun  15168  prodeq1f  15254  fprod2d  15327  lcmfunsnlem  15975  coprmprod  15995  vdwmc  16304  prmgaplem3  16379  prmgaplem4  16380  restsspw  16697  ismred2  16866  mrcval  16873  mrcuni  16884  acsfn  16922  isssc  17082  drsdirfi  17540  ipodrsima  17767  cntzssv  18450  pmtrfrn  18578  pmtrrn2  18580  pmtrdifellem1  18596  pmtrdifellem2  18597  sylow2alem2  18735  sylow2a  18736  efgval  18835  gsumzaddlem  19034  ablfac1eulem  19187  lspval  19740  lspindpi  19897  znf1o  20243  zntoslem  20248  aspval  20559  mplsubglem  20672  mpllsslem  20673  mplcoe1  20705  mplcoe5  20708  mdetunilem9  21225  uniopn  21502  fiinopn  21506  fiinbas  21557  baspartn  21559  eltg2  21563  eltg3  21567  topbas  21577  pptbas  21613  clsval  21642  neiint  21709  neips  21718  opnneissb  21719  opnssneib  21720  innei  21730  neiptoptop  21736  neiptopnei  21737  restbas  21763  restcld  21777  neitr  21785  restcls  21786  restntr  21787  cnpdis  21898  cmpsublem  22004  cmpsub  22005  fiuncmp  22009  unconn  22034  1stcfb  22050  2ndc1stc  22056  1stcrest  22058  2ndcctbss  22060  2ndcomap  22063  dis2ndc  22065  lly1stc  22101  refssex  22116  refun0  22120  llycmpkgen2  22155  txbas  22172  eltx  22173  ptuni2  22181  neitx  22212  ptpjopn  22217  ptcld  22218  txlm  22253  tx1stc  22255  txkgen  22257  xkopt  22260  xkococnlem  22264  ptcmpfi  22418  fbssfi  22442  opnfbas  22447  isfil2  22461  isfildlem  22462  snfil  22469  fsubbas  22472  ssfg  22477  fgss2  22479  fgcl  22483  fbasrn  22489  fgtr  22495  ufli  22519  uffix  22526  rnelfmlem  22557  fclscf  22630  alexsublem  22649  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALTlem4  22655  alexsubALT  22656  tmdgsum2  22701  subgntr  22712  opnsubg  22713  qustgpopn  22725  tsmsfbas  22733  tsmsgsum  22744  tsmsres  22749  tsmsf1o  22750  tsmsxplem1  22758  tsmsxp  22760  isust  22809  ustssel  22811  ustincl  22813  ustdiag  22814  ustinvel  22815  ustexhalf  22816  ustexsym  22821  ust0  22825  restutop  22843  ustuqtop4  22850  utopsnneiplem  22853  blssexps  23033  blssex  23034  neibl  23108  blcld  23112  met1stc  23128  met2ndci  23129  metrest  23131  prdsxmslem2  23136  metustfbas  23164  cfilucfil  23166  metuel2  23172  metustbl  23173  restmetu  23177  dscopn  23180  isngp2  23203  tgioo  23401  tgqioo  23405  zdis  23421  xrge0tsms  23439  fsumcn  23475  volivth  24211  vitalilem2  24213  itgfsum  24430  limcun  24498  recnprss  24507  dvmptfsum  24578  ftc1a  24640  plyssc  24797  efopn  25249  jensen  25574  tglnunirn  26342  lpvtx  26861  umgredgprv  26900  usgredgprvALT  26985  issubgr2  27062  subgrprop2  27064  egrsubgr  27067  0uhgrsubgr  27069  frcond3  28054  hhsssh  29052  shintcl  29113  chintcl  29115  spanval  29116  omlsi  29187  pjoml  29219  chnlen0  29227  chsscon3  29283  chlejb1  29295  chnle  29297  spanun  29328  h1datom  29365  cmbr4i  29384  pjoml2  29394  pjoml3  29395  lecm  29400  osumcor2i  29427  osum  29428  spansncv  29436  pjcjt2  29475  pjopyth  29503  hstel2  30002  stj  30018  stcltr1i  30057  mdi  30078  mdbr3  30080  mdbr4  30081  dmdbr  30082  dmdmd  30083  dmdbr5  30091  mdsl1i  30104  mdslmd1lem3  30110  mdslmd1lem4  30111  mdslmd1i  30112  csmdsymi  30117  atss  30129  atom1d  30136  superpos  30137  chcv1  30138  shatomici  30141  shatomistici  30144  hatomistici  30145  chrelat2  30153  chirredi  30177  atcvat4i  30180  mdsymlem2  30187  mdsymlem6  30191  dmdbr6ati  30206  dmdbr7ati  30207  xrge0tsmsd  30742  gsumle  30775  gsumvsca1  30904  gsumvsca2  30905  prmidl  31023  ismxidl  31042  zarcls1  31222  zarclsun  31223  zarclsiin  31224  zarclsint  31225  zarclssn  31226  zartop  31229  zartopon  31230  zart0  31232  zarmxt1  31233  zarcmp  31235  rhmpreimacnlem  31237  rhmpreimacn  31238  tpr2rico  31265  issiga  31481  isrnsiga  31482  sigagenval  31509  measiuns  31586  dya2icoseg  31645  dya2iocnrect  31649  dya2iocuni  31651  carsgmon  31682  carsgsigalem  31683  carsgclctunlem2  31687  carsgclctun  31689  pmeasmono  31692  pmeasadd  31693  bnj517  32267  bnj1118  32366  bnj1145  32375  bnj1154  32381  bnj1452  32434  bnj1498  32443  pthhashvtx  32487  kur14lem1  32566  cvmopnlem  32638  dfon2lem3  33143  dfon2lem7  33147  frmin  33197  frrlem1  33236  frrlem13  33248  brsslt  33367  brsset  33463  fness  33810  fneref  33811  fnessref  33818  neibastop2lem  33821  topmeet  33825  fnejoin2  33830  tailfb  33838  filnetlem4  33842  onsucsuccmpi  33904  bj-snglss  34406  bj-restpw  34507  bj-imdirco  34605  dissneqlem  34757  relowlssretop  34780  relowlpssretop  34781  ctbssinf  34823  pibt2  34834  matunitlindflem1  35053  ptrecube  35057  poimirlem29  35086  mblfinlem2  35095  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  indexa  35171  indexdom  35172  neificl  35191  istotbnd3  35209  sstotbnd2  35212  sstotbnd  35213  equivtotbnd  35216  ssbnd  35226  heiborlem1  35249  heiborlem6  35254  heiborlem8  35256  heiborlem10  35258  unichnidl  35469  pridl  35475  ismaxidl  35478  igenval  35499  igenval2  35504  ispridlc  35508  relcnveq3  35738  iss2  35761  elrelscnveq3  35891  brssr  35901  lsmsat  36304  lssatomic  36307  lssats  36308  lsat0cv  36329  lcvexchlem4  36333  lcvexchlem5  36334  lsatcvatlem  36345  l1cvpat  36350  ispsubsp  37041  linepsubN  37048  pclvalN  37186  ispsubclN  37233  ispsubcl2N  37243  pclfinclN  37246  diaelrnN  38341  docavalN  38419  dochval  38647  dvh4dimat  38734  dochexmidlem1  38756  lpolconN  38783  mapdordlem2  38933  ismrcd1  39639  ismrcd2  39640  ismrc  39642  mzpcompact2lem  39692  aomclem6  40003  hbtlem6  40073  rgspnval  40112  ssficl  40268  ssuncl  40269  ssdifcl  40270  sssymdifcl  40271  elmapintrab  40276  clcnvlem  40323  iunrelexpmin1  40409  iunrelexpmin2  40413  clsk3nimkb  40743  clsk1indlem1  40748  isotone1  40751  isotone2  40752  ntrclsiso  40770  gneispace  40837  gneispacess2  40849  onfrALTlem5  41248  onfrALTlem5VD  41591  islptre  42261  dvmptconst  42557  dvmptidg  42559  dvmulcncf  42567  dvdivcncf  42569  dvmptfprod  42587  stoweidlem51  42693  stoweidlem52  42694  fourierdlem103  42851  fourierdlem104  42852  ioorrnopnlem  42946  ioorrnopnxrlem  42948  salgenval  42963  ovnval2  43184  ovncvrrp  43203  ovnsubaddlem1  43209  ovnsubadd  43211  ovncvr2  43250  hspmbl  43268  elsetpreimafvssdm  43903  uspgrsprfo  44376  setrec1lem1  45217  setrec1lem4  45220  setrec2fun  45222  elsetrecslem  45228  elpglem2  45241