Theorem sseq2 3965

Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)

Assertion

Ref	Expression
sseq2	⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Proof of Theorem sseq2

Step	Hyp	Ref	Expression
1		eqss 3954	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3946	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 33	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3946	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
5	4	com12 33	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
6	3, 5	anbiim 652	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
7	1, 6	sylbi 220	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  sseq12  3966  sseq2i  3968  sseq2d  3971  nssne1  4001  psseq2  4047  sseq0  4360  un00  4402  disjpss  4418  pweqALT  4573  ssintab  4925  ssintub  4926  intmin  4928  treq  5218  al0ssb  5262  sseliALT  5263  ssexg  5283  intabs  5309  iunopeqop  5494  iunopeqopOLD  5495  onelssex  6399  ordunidif  6400  ordssun  6454  fununi  6600  feq3  6675  ssimaexg  6957  fnssintima  7350  iunpw  7758  tfindsg  7845  limomss  7855  findsg  7882  funcnvuni  7917  frxp  8110  frrlem1  8271  frrlem13  8283  onfununi  8316  oawordeu  8528  oawordexr  8529  nnawordex  8611  eldifsucnn  8638  coflton  8645  cofon1  8646  cofon2  8647  cofonr  8648  naddcllem  8650  naddunif  8668  ereq1  8690  xpider  8774  domeng  8947  sbthlem4  9066  sbthlem5  9067  domssex  9114  ssfi  9145  finsschain  9304  dffi2  9371  dffi3  9379  hartogslem1  9492  inf3lema  9581  cantnflem1  9646  dfttrcl2  9681  tz9.1  9686  tz9.1c  9687  tctr  9695  tcmin  9696  tcrank  9844  scottex  9847  cardlim  9946  infxpenlem  9985  infxpenc2  9994  isinfcard  10064  alephinit  10067  alephval3  10082  dfac3  10093  cflem  10216  cflemOLD  10217  cfval  10218  cflecard  10224  cfsuc  10229  cff1  10230  cfflb  10231  cflim2  10235  isf32lem2  10326  fin1a2lem13  10384  ac7g  10446  ttukeylem5  10485  ttukeylem7  10487  pwcfsdom  10556  pwfseqlem5  10636  pwfseq  10637  gch2  10648  winalim  10668  wunex  10712  wuncss  10718  eltskg  10723  eltsk2g  10724  gruina  10791  grur1a  10792  axgroth6  10801  swrdnd2  14681  trcleq2lem  15016  dfrtrcl2  15087  fprodss  15990  mrcflem  17650  mrcval  17654  isacs2  17697  acsfiel  17698  ipoval  18574  fpwipodrs  18584  ipodrsima  18585  mreclatBAD  18607  slwispgp  19669  pgpssslw  19672  lsmss1b  19724  lsmss2b  19726  cntzcmnss  19899  gsumzres  19967  rgspnval  20685  rgspncl  20686  rgspnmin  20688  lspf  21061  lspval  21062  lbsextlem1  21248  lbsextlem3  21250  lbsextlem4  21251  unichnlidl  21328  isprmidl  21422  ssdifidllem  21441  ssdifidl  21442  ssdifidlprm  21443  aspval  21979  mplsubglem  22105  mpllsslem  22106  basis2  23065  eltg2  23072  clsval  23151  clscld  23161  clsval2  23164  ntrcls0  23190  isnei  23217  neiint  23218  neips  23227  opnneissb  23228  opnssneib  23229  neindisj2  23237  innei  23239  neiptoptop  23245  neiptopnei  23246  neitr  23294  restcls  23295  cnpimaex  23370  cnprest2  23404  regsep  23448  nrmsep3  23469  nrmsep  23471  regsep2  23490  tgcmp  23515  uncmp  23517  bwth  23524  1stcfb  23559  1stcrest  23567  2ndcctbss  23569  1stcelcls  23575  lly1stc  23610  ssref  23626  refref  23627  comppfsc  23646  xkoopn  23703  neitx  23721  txcnp  23734  txcmplem1  23755  kqnrmlem1  23857  kqnrmlem2  23858  nrmhmph  23908  fbssfi  23951  opnfbas  23956  fbasfip  23982  fbunfip  23983  fgss2  23988  fgcl  23992  supfil  24009  isufil2  24022  filssufilg  24025  ssufl  24032  ufileu  24033  elfm3  24064  fmfnfm  24072  ufldom  24076  fbflim2  24091  flfneii  24106  flftg  24110  txflf  24120  supnfcls  24134  fclscf  24139  fclsfnflim  24141  flimfnfcls  24142  alexsubALTlem2  24162  alexsubALTlem3  24163  alexsubALTlem4  24164  alexsubALT  24165  tsmsfbas  24242  tsmsres  24258  tsmsf1o  24259  tsmsxplem1  24267  tsmsxp  24269  ustssel  24320  ustincl  24322  ustdiag  24323  ustinvel  24324  ustexhalf  24325  ust0  24334  elutop  24347  ustuqtop4  24358  cfiluexsm  24403  cfiluweak  24408  blssps  24538  blss  24539  metss  24622  metrest  24638  metcnp3  24654  metnrmlem3  24976  lebnumlem3  25079  lebnum  25080  ellimc3  25995  lhop1lem  26129  dchrelbas  27354  eqcuts2  27933  cutsun12  27937  madebdayim  28035  madebday  28047  oniso  28418  bdayn0p1  28516  prlngd  29120  upgredgpr  29397  dfnbgr3  29593  nbupgr  29599  nbumgrvtx  29601  nbgr2vtx1edg  29605  nbuhgr2vtx1edgb  29607  cusgrexilem2  29697  wlkvtxiedg  29879  wlkres  29923  upgr1wlkdlem2  30402  1pthon2v  30409  1pthon2ve  30410  cusconngr  30447  isfrgr  30516  avril1  30719  spanval  31590  spancl  31593  shsval2i  31644  omlsi  31661  ococin  31665  chsupsn  31670  pjoml  31693  shs00i  31707  chj00i  31744  chsscon3  31757  chlejb1  31769  chnle  31771  pjoml2  31868  pjoml3  31869  lecm  31874  stcltr1i  32531  mdbr  32551  dmdmd  32557  dmdi  32559  dmdbr3  32562  dmdbr4  32563  mdsl1i  32578  mdslmd1lem3  32584  mdslmd1lem4  32585  csmdsymi  32591  hatomic  32617  chrelat2  32627  atord  32645  atcvat4i  32654  fz1nntr  33055  elrgspnlem4  33473  fldgenval  33543  fldgensdrg  33545  fldgenssv  33546  fldgenssp  33549  nsgmgc  33632  nsgqusf1olem2  33634  mxidlmax  33660  ssmxidllem  33668  ssmxidl  33669  dflringlem  33696  1arithufdlem4  33749  reff  34141  cmpcref  34152  zarcls1  34171  zarclsiin  34173  zarclssn  34175  zart0  34181  zarmxt1  34182  zarcmp  34184  rhmpreimacnlem  34186  sigagenval  34442  dmsigagen  34446  sigagenss  34451  ldsysgenld  34462  ldgenpisyslem1  34465  ldgenpisyslem2  34466  dynkin  34469  carsgmon  34616  carsgclctunlem2  34621  bnj1286  35319  bnj1452  35352  fineqvac  35419  tz9.1regs  35437  onvf1odlem4  35456  vonf1wev  35458  vonf1owevOLD  35460  kur14lem9  35572  mclsssvlem  35920  mclsind  35928  imagesset  36311  altopthsn  36319  fnessref  36725  refssfne  36726  topjoin  36733  neifg  36739  tz9.1tco  36851  ttc00  36876  dfttc3gw  36891  bj-snglex  37465  bj-imdirvallem  37679  relowlssretop  37864  relowlpssretop  37865  exrecfnlem  37880  finxpreclem3  37894  pibt2  37918  poimirlem29  38155  poimir  38159  mblfinlem3  38165  totbndss  38283  heibor1lem  38315  unichnidl  38537  ispridl  38540  maxidlmax  38549  igenval  38567  igenidl  38569  igenmin  38570  igenval2  38572  dfsuccl4  38980  brssr  39087  suceldisj  39324  lsatcmp  39634  lcvexchlem4  39668  lcvexchlem5  39669  pclvalN  40521  pclclN  40522  elpcliN  40524  docaclN  41755  dihglb2  41973  doch2val2  41995  dochocss  41997  dochexmidlem7  42097  lpolconN  42118  mapdval  42259  nacsfix  43300  mzpcompact2  43340  superficl  44150  superuncl  44151  cleq2lem  44191  clcnvlem  44206  dfrtrcl3  44316  clsk1indlem2  44625  neik0pk1imk0  44630  isotone1  44631  isotone2  44632  ntrclsiso  44650  gneispacess2  44729  mnuunid  44846  mnurndlem2  44851  ssrecnpr  44877  founiiun  45756  founiiun0  45767  islptre  46194  salgenval  46894  salgenn0  46904  salgencl  46905  sssalgen  46908  salgenss  46909  salgenuni  46910  issalgend  46911  dfsalgen2  46914  salgencntex  46916  dfclnbgr3  48447  predgclnbgrel  48460  clnbgredg  48461  clnbgrgrimlem  48554  clnbgrgrim  48555  opndisj  49533  opnneilem  49536  sepfsepc  49558  iscnrm3rlem8  49577  iscnrm3llem2  49580  intubeu  49614  ipolubdm  49617  ipoglbdm  49620  setrec1lem1  50317  setrec1lem3  50319  setrec2fun  50322