Theorem sseq2 3966

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 3955	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3947	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 33	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3947	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
5	4	com12 33	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
6	3, 5	anbiim 653	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
7	1, 6	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  sseq2i  3969  sseq2d  3972  nssne1  4002  psseq2  4048  sseq0b  4363  un00  4367  disjpss  4424  pweqALT  4582  ssintab  4935  ssintub  4936  intmin  4938  treq  5230  al0ssb  5276  sseliALT  5277  ssexgOLD  5299  intabs  5324  iunopeqop  5509  iunopeqopOLD  5510  onelssex  6417  ordunidif  6418  ordssun  6472  fununi  6618  feq3  6692  ssimaexg  6974  fnssintima  7373  iunpw  7779  tfindsg  7866  limomss  7876  findsg  7903  funcnvuni  7938  frxp  8131  frrlem1  8292  frrlem13  8304  onfununi  8337  oawordeu  8549  oawordexr  8550  nnawordex  8632  eldifsucnn  8659  coflton  8666  cofon1  8667  cofon2  8668  cofonr  8669  naddcllem  8671  naddunif  8689  ereq1  8711  xpider  8795  domeng  8968  sbthlem4  9088  sbthlem5  9089  domssex  9136  ssfi  9167  finsschain  9326  dffi2  9393  dffi3  9401  hartogslem1  9514  inf3lema  9603  cantnflem1  9668  dfttrcl2  9703  tz9.1  9708  tz9.1c  9709  tctr  9717  tcmin  9718  tcrank  9866  scottex  9872  scottexOLD  9873  cardlim  9977  infxpenlem  10016  infxpenc2  10025  isinfcard  10095  alephinit  10098  alephval3  10113  dfac3  10124  cflem  10247  cfval  10248  cflecard  10254  cfsuc  10259  cff1  10260  cfflb  10261  cflim2  10265  isf32lem2  10356  fin1a2lem13  10414  ac7g  10476  ttukeylem5  10515  ttukeylem7  10517  pwcfsdom  10586  pwfseqlem5  10666  pwfseq  10667  gch2  10678  winalim  10698  wunex  10742  wuncss  10748  eltskg  10753  eltsk2g  10754  gruina  10821  grur1a  10822  axgroth6  10831  swrdnd2  14717  trcleq2lem  15054  dfrtrcl2  15125  fprodss  16028  mrcflem  17687  mrcval  17691  isacs2  17734  acsfiel  17735  ipoval  18611  fpwipodrs  18621  ipodrsima  18622  mreclatBAD  18644  slwispgp  19712  pgpssslw  19715  lsmss1b  19767  lsmss2b  19769  cntzcmnss  19942  gsumzres  20010  rgspnval  20748  rgspncl  20749  rgspnmin  20751  lspf  21132  lspval  21133  lbsextlem1  21319  lbsextlem3  21321  lbsextlem4  21322  unichnlidl  21399  rspprop  21407  isprmidl  21500  ssdifidllem  21521  ssdifidl  21522  ssdifidlprm  21523  aspval  22059  mplsubglem  22185  mpllsslem  22186  basis2  23145  eltg2  23152  clsval  23231  clscld  23241  clsval2  23244  ntrcls0  23270  isnei  23297  neiint  23298  neips  23307  opnneissb  23308  opnssneib  23309  neindisj2  23317  innei  23319  neiptoptop  23325  neiptopnei  23326  neitr  23374  restcls  23375  cnpimaex  23450  cnprest2  23484  regsep  23528  nrmsep3  23549  nrmsep  23551  regsep2  23570  tgcmp  23595  uncmp  23597  bwth  23604  1stcfb  23639  1stcrest  23647  2ndcctbss  23649  1stcelcls  23655  lly1stc  23690  ssref  23706  refref  23707  comppfsc  23726  xkoopn  23783  neitx  23801  txcnp  23814  txcmplem1  23835  kqnrmlem1  23937  kqnrmlem2  23938  nrmhmph  23988  fbssfi  24031  opnfbas  24036  fbasfip  24062  fbunfip  24063  fgss2  24068  fgcl  24072  supfil  24089  isufil2  24102  filssufilg  24105  ssufl  24112  ufileu  24113  elfm3  24144  fmfnfm  24152  ufldom  24156  fbflim2  24171  flfneii  24186  flftg  24190  txflf  24200  supnfcls  24214  fclscf  24219  fclsfnflim  24221  flimfnfcls  24222  alexsubALTlem2  24242  alexsubALTlem3  24243  alexsubALTlem4  24244  alexsubALT  24245  tsmsfbas  24322  tsmsres  24338  tsmsf1o  24339  tsmsxplem1  24347  tsmsxp  24349  ustssel  24400  ustincl  24402  ustdiag  24403  ustinvel  24404  ustexhalf  24405  ust0  24414  elutop  24427  ustuqtop4  24438  cfiluexsm  24483  cfiluweak  24488  blssps  24618  blss  24619  metss  24702  metrest  24718  metcnp3  24734  metnrmlem3  25056  lebnumlem3  25159  lebnum  25160  ellimc3  26075  lhop1lem  26209  dchrelbas  27437  eqcuts2  28016  cutsun12  28020  madebdayim  28118  madebday  28130  oniso  28501  bdayn0p1  28599  prlngd  29226  dfprlng2  29234  upgredgpr  29529  dfnbgr3  29725  nbupgr  29731  nbumgrvtx  29733  nbgr2vtx1edg  29737  nbuhgr2vtx1edgb  29739  cusgrexilem2  29829  wlkvtxiedg  30011  wlkres  30055  upgr1wlkdlem2  30534  1pthon2v  30541  1pthon2ve  30542  cusconngr  30579  isfrgr  30648  avril1  30851  spanval  31722  spancl  31725  shsval2i  31776  omlsi  31793  ococin  31797  chsupsn  31802  pjoml  31825  shs00i  31839  chj00i  31876  chsscon3  31889  chlejb1  31901  chnle  31903  pjoml2  32000  pjoml3  32001  lecm  32006  stcltr1i  32663  mdbr  32683  dmdmd  32689  dmdi  32691  dmdbr3  32694  dmdbr4  32695  mdsl1i  32710  mdslmd1lem3  32716  mdslmd1lem4  32717  csmdsymi  32723  hatomic  32749  chrelat2  32759  atord  32777  atcvat4i  32786  fz1nntr  33184  elrgspnlem4  33596  fldgenval  33664  fldgensdrg  33666  fldgenssv  33667  fldgenssp  33670  nsgmgc  33752  nsgqusf1olem2  33754  mxidlmax  33779  ssmxidllem  33787  ssmxidl  33788  dflringlem  33815  1arithufdlem4  33868  reff  34260  cmpcref  34271  zarcls1  34290  zarclsiin  34292  zarclssn  34294  zart0  34300  zarmxt1  34301  zarcmp  34303  rhmpreimacnlem  34305  sigagenval  34562  dmsigagen  34566  sigagenss  34571  ldsysgenld  34582  ldgenpisyslem1  34585  ldgenpisyslem2  34586  dynkin  34589  carsgmon  34736  carsgclctunlem2  34741  bnj1286  35439  bnj1452  35472  fineqvac  35553  tz9.1regs  35571  onvf1odlem4  35614  vonf1wev  35616  vonf1owevOLD  35618  kur14lem9  35727  mclsssvlem  36075  mclsind  36083  imagesset  36466  altopthsn  36474  fnessref  36909  refssfne  36910  topjoin  36917  neifg  36923  tz9.1tco  37035  ttc00  37060  dfttc3gw  37075  bj-snglex  37650  bj-imdirvallem  37865  relowlssretop  38050  relowlpssretop  38051  exrecfnlem  38066  finxpreclem3  38080  pibt2  38104  poimirlem29  38341  poimir  38345  mblfinlem3  38351  totbndss  38469  heibor1lem  38501  unichnidl  38723  ispridl  38726  maxidlmax  38735  igenval  38753  igenidl  38755  igenmin  38756  igenval2  38758  dfsuccl4  39164  brssr  39271  suceldisj  39508  lsatcmp  39818  lcvexchlem4  39852  lcvexchlem5  39853  pclvalN  40705  pclclN  40706  elpcliN  40708  docaclN  41939  dihglb2  42157  doch2val2  42179  dochocss  42181  dochexmidlem7  42281  lpolconN  42302  mapdval  42443  nacsfix  43484  mzpcompact2  43524  superficl  44334  superuncl  44335  cleq2lem  44375  clcnvlem  44390  dfrtrcl3  44500  clsk1indlem2  44809  neik0pk1imk0  44814  isotone1  44815  isotone2  44816  ntrclsiso  44834  gneispacess2  44913  mnuunid  45028  mnurndlem2  45033  ssrecnpr  45059  founiiun  45938  founiiun0  45949  islptre  46376  salgenval  47076  salgenn0  47086  salgencl  47087  sssalgen  47090  salgenss  47091  salgenuni  47092  issalgend  47093  dfsalgen2  47096  salgencntex  47098  dfclnbgr3  48632  predgclnbgrel  48645  clnbgredg  48646  clnbgrgrimlem  48739  clnbgrgrim  48740  opndisj  49722  opnneilem  49725  sepfsepc  49747  iscnrm3rlem8  49766  iscnrm3llem2  49769  intubeu  49803  ipolubdm  49806  ipoglbdm  49809  setrec1lem1  50506  setrec1lem3  50508  setrec2fun  50511