Theorem sseq2 3964

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 3953	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3945	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 33	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3945	. . . 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 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  sseq12  3965  sseq2i  3967  sseq2d  3970  nssne1  4000  psseq2  4046  sseq0b  4361  un00  4365  disjpss  4422  pweqALT  4578  ssintab  4931  ssintub  4932  intmin  4934  treq  5226  al0ssb  5272  sseliALT  5273  ssexgOLD  5295  intabs  5321  iunopeqop  5506  iunopeqopOLD  5507  onelssex  6412  ordunidif  6413  ordssun  6467  fununi  6613  feq3  6687  ssimaexg  6969  fnssintima  7362  iunpw  7771  tfindsg  7858  limomss  7868  findsg  7895  funcnvuni  7930  frxp  8123  frrlem1  8284  frrlem13  8296  onfununi  8329  oawordeu  8541  oawordexr  8542  nnawordex  8624  eldifsucnn  8651  coflton  8658  cofon1  8659  cofon2  8660  cofonr  8661  naddcllem  8663  naddunif  8681  ereq1  8703  xpider  8787  domeng  8960  sbthlem4  9079  sbthlem5  9080  domssex  9127  ssfi  9158  finsschain  9317  dffi2  9384  dffi3  9392  hartogslem1  9505  inf3lema  9594  cantnflem1  9659  dfttrcl2  9694  tz9.1  9699  tz9.1c  9700  tctr  9708  tcmin  9709  tcrank  9857  scottex  9860  cardlim  9959  infxpenlem  9998  infxpenc2  10007  isinfcard  10077  alephinit  10080  alephval3  10095  dfac3  10106  cflem  10229  cflemOLD  10230  cfval  10231  cflecard  10237  cfsuc  10242  cff1  10243  cfflb  10244  cflim2  10248  isf32lem2  10339  fin1a2lem13  10397  ac7g  10459  ttukeylem5  10498  ttukeylem7  10500  pwcfsdom  10569  pwfseqlem5  10649  pwfseq  10650  gch2  10661  winalim  10681  wunex  10725  wuncss  10731  eltskg  10736  eltsk2g  10737  gruina  10804  grur1a  10805  axgroth6  10814  swrdnd2  14695  trcleq2lem  15030  dfrtrcl2  15101  fprodss  16004  mrcflem  17663  mrcval  17667  isacs2  17710  acsfiel  17711  ipoval  18587  fpwipodrs  18597  ipodrsima  18598  mreclatBAD  18620  slwispgp  19682  pgpssslw  19685  lsmss1b  19737  lsmss2b  19739  cntzcmnss  19912  gsumzres  19980  rgspnval  20698  rgspncl  20699  rgspnmin  20701  lspf  21076  lspval  21077  lbsextlem1  21263  lbsextlem3  21265  lbsextlem4  21266  unichnlidl  21343  rspprop  21351  isprmidl  21444  ssdifidllem  21465  ssdifidl  21466  ssdifidlprm  21467  aspval  22003  mplsubglem  22129  mpllsslem  22130  basis2  23089  eltg2  23096  clsval  23175  clscld  23185  clsval2  23188  ntrcls0  23214  isnei  23241  neiint  23242  neips  23251  opnneissb  23252  opnssneib  23253  neindisj2  23261  innei  23263  neiptoptop  23269  neiptopnei  23270  neitr  23318  restcls  23319  cnpimaex  23394  cnprest2  23428  regsep  23472  nrmsep3  23493  nrmsep  23495  regsep2  23514  tgcmp  23539  uncmp  23541  bwth  23548  1stcfb  23583  1stcrest  23591  2ndcctbss  23593  1stcelcls  23599  lly1stc  23634  ssref  23650  refref  23651  comppfsc  23670  xkoopn  23727  neitx  23745  txcnp  23758  txcmplem1  23779  kqnrmlem1  23881  kqnrmlem2  23882  nrmhmph  23932  fbssfi  23975  opnfbas  23980  fbasfip  24006  fbunfip  24007  fgss2  24012  fgcl  24016  supfil  24033  isufil2  24046  filssufilg  24049  ssufl  24056  ufileu  24057  elfm3  24088  fmfnfm  24096  ufldom  24100  fbflim2  24115  flfneii  24130  flftg  24134  txflf  24144  supnfcls  24158  fclscf  24163  fclsfnflim  24165  flimfnfcls  24166  alexsubALTlem2  24186  alexsubALTlem3  24187  alexsubALTlem4  24188  alexsubALT  24189  tsmsfbas  24266  tsmsres  24282  tsmsf1o  24283  tsmsxplem1  24291  tsmsxp  24293  ustssel  24344  ustincl  24346  ustdiag  24347  ustinvel  24348  ustexhalf  24349  ust0  24358  elutop  24371  ustuqtop4  24382  cfiluexsm  24427  cfiluweak  24432  blssps  24562  blss  24563  metss  24646  metrest  24662  metcnp3  24678  metnrmlem3  25000  lebnumlem3  25103  lebnum  25104  ellimc3  26019  lhop1lem  26153  dchrelbas  27381  eqcuts2  27960  cutsun12  27964  madebdayim  28062  madebday  28074  oniso  28445  bdayn0p1  28543  prlngd  29170  dfprlng2  29178  upgredgpr  29473  dfnbgr3  29669  nbupgr  29675  nbumgrvtx  29677  nbgr2vtx1edg  29681  nbuhgr2vtx1edgb  29683  cusgrexilem2  29773  wlkvtxiedg  29955  wlkres  29999  upgr1wlkdlem2  30478  1pthon2v  30485  1pthon2ve  30486  cusconngr  30523  isfrgr  30592  avril1  30795  spanval  31666  spancl  31669  shsval2i  31720  omlsi  31737  ococin  31741  chsupsn  31746  pjoml  31769  shs00i  31783  chj00i  31820  chsscon3  31833  chlejb1  31845  chnle  31847  pjoml2  31944  pjoml3  31945  lecm  31950  stcltr1i  32607  mdbr  32627  dmdmd  32633  dmdi  32635  dmdbr3  32638  dmdbr4  32639  mdsl1i  32654  mdslmd1lem3  32660  mdslmd1lem4  32661  csmdsymi  32667  hatomic  32693  chrelat2  32703  atord  32721  atcvat4i  32730  fz1nntr  33128  elrgspnlem4  33546  fldgenval  33614  fldgensdrg  33616  fldgenssv  33617  fldgenssp  33620  nsgmgc  33702  nsgqusf1olem2  33704  mxidlmax  33729  ssmxidllem  33737  ssmxidl  33738  dflringlem  33765  1arithufdlem4  33818  reff  34210  cmpcref  34221  zarcls1  34240  zarclsiin  34242  zarclssn  34244  zart0  34250  zarmxt1  34251  zarcmp  34253  rhmpreimacnlem  34255  sigagenval  34511  dmsigagen  34515  sigagenss  34520  ldsysgenld  34531  ldgenpisyslem1  34534  ldgenpisyslem2  34535  dynkin  34538  carsgmon  34685  carsgclctunlem2  34690  bnj1286  35388  bnj1452  35421  fineqvac  35510  tz9.1regs  35528  onvf1odlem4  35571  vonf1wev  35573  vonf1owevOLD  35575  kur14lem9  35687  mclsssvlem  36035  mclsind  36043  imagesset  36426  altopthsn  36434  fnessref  36849  refssfne  36850  topjoin  36857  neifg  36863  tz9.1tco  36975  ttc00  37000  dfttc3gw  37015  bj-snglex  37590  bj-imdirvallem  37805  relowlssretop  37990  relowlpssretop  37991  exrecfnlem  38006  finxpreclem3  38020  pibt2  38044  poimirlem29  38281  poimir  38285  mblfinlem3  38291  totbndss  38409  heibor1lem  38441  unichnidl  38663  ispridl  38666  maxidlmax  38675  igenval  38693  igenidl  38695  igenmin  38696  igenval2  38698  dfsuccl4  39104  brssr  39211  suceldisj  39448  lsatcmp  39758  lcvexchlem4  39792  lcvexchlem5  39793  pclvalN  40645  pclclN  40646  elpcliN  40648  docaclN  41879  dihglb2  42097  doch2val2  42119  dochocss  42121  dochexmidlem7  42221  lpolconN  42242  mapdval  42383  nacsfix  43426  mzpcompact2  43466  superficl  44276  superuncl  44277  cleq2lem  44317  clcnvlem  44332  dfrtrcl3  44442  clsk1indlem2  44751  neik0pk1imk0  44756  isotone1  44757  isotone2  44758  ntrclsiso  44776  gneispacess2  44855  mnuunid  44970  mnurndlem2  44975  ssrecnpr  45001  founiiun  45880  founiiun0  45891  islptre  46318  salgenval  47018  salgenn0  47028  salgencl  47029  sssalgen  47032  salgenss  47033  salgenuni  47034  issalgend  47035  dfsalgen2  47038  salgencntex  47040  dfclnbgr3  48574  predgclnbgrel  48587  clnbgredg  48588  clnbgrgrimlem  48681  clnbgrgrim  48682  opndisj  49664  opnneilem  49667  sepfsepc  49689  iscnrm3rlem8  49708  iscnrm3llem2  49711  intubeu  49745  ipolubdm  49748  ipoglbdm  49751  setrec1lem1  50448  setrec1lem3  50450  setrec2fun  50453