Theorem sseq2 3957

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 3946	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3937	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3937	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
5	4	com12 32	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
6	3, 5	anbiim 641	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
7	1, 6	sylbi 217	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  sseq12  3958  sseq2i  3960  sseq2d  3963  nssne1  3993  psseq2  4040  sseq0  4352  un00  4394  disjpss  4410  pweqALT  4566  ssintab  4917  ssintub  4918  intmin  4920  treq  5209  al0ssb  5250  sseliALT  5251  ssexg  5265  intabs  5291  iunopeqop  5466  onelssex  6362  ordunidif  6363  ordssun  6417  fununi  6563  feq3  6638  ssimaexg  6916  fnssintima  7304  iunpw  7712  tfindsg  7799  limomss  7809  findsg  7835  funcnvuni  7870  frxp  8064  frrlem1  8224  frrlem13  8236  onfununi  8269  oawordeu  8478  oawordexr  8479  nnawordex  8560  eldifsucnn  8587  coflton  8594  cofon1  8595  cofon2  8596  cofonr  8597  naddcllem  8599  naddunif  8616  ereq1  8637  xpider  8720  domeng  8893  sbthlem4  9012  sbthlem5  9013  domssex  9060  ssfi  9091  finsschain  9252  dffi2  9316  dffi3  9324  hartogslem1  9437  inf3lema  9523  cantnflem1  9588  dfttrcl2  9623  tz9.1  9628  tz9.1c  9629  tctr  9637  tcmin  9638  tcrank  9786  scottex  9787  cardlim  9874  infxpenlem  9913  infxpenc2  9922  isinfcard  9992  alephinit  9995  alephval3  10010  dfac3  10021  cflem  10145  cflemOLD  10146  cfval  10147  cflecard  10153  cfsuc  10157  cff1  10158  cfflb  10159  cflim2  10163  isf32lem2  10254  fin1a2lem13  10312  ac7g  10374  ttukeylem5  10413  ttukeylem7  10415  pwcfsdom  10483  pwfseqlem5  10563  pwfseq  10564  gch2  10575  winalim  10595  wunex  10639  wuncss  10645  eltskg  10650  eltsk2g  10651  gruina  10718  grur1a  10719  axgroth6  10728  swrdnd2  14567  trcleq2lem  14902  dfrtrcl2  14973  fprodss  15859  mrcflem  17516  mrcval  17520  isacs2  17563  acsfiel  17564  ipoval  18440  fpwipodrs  18450  ipodrsima  18451  mreclatBAD  18473  slwispgp  19527  pgpssslw  19530  lsmss1b  19582  lsmss2b  19584  cntzcmnss  19757  gsumzres  19825  rgspnval  20531  rgspncl  20532  rgspnmin  20534  lspf  20911  lspval  20912  lbsextlem1  21099  lbsextlem3  21101  lbsextlem4  21102  aspval  21814  mplsubglem  21939  mpllsslem  21940  basis2  22869  eltg2  22876  clsval  22955  clscld  22965  clsval2  22968  ntrcls0  22994  isnei  23021  neiint  23022  neips  23031  opnneissb  23032  opnssneib  23033  neindisj2  23041  innei  23043  neiptoptop  23049  neiptopnei  23050  neitr  23098  restcls  23099  cnpimaex  23174  cnprest2  23208  regsep  23252  nrmsep3  23273  nrmsep  23275  regsep2  23294  tgcmp  23319  uncmp  23321  bwth  23328  1stcfb  23363  1stcrest  23371  2ndcctbss  23373  1stcelcls  23379  lly1stc  23414  ssref  23430  refref  23431  comppfsc  23450  xkoopn  23507  neitx  23525  txcnp  23538  txcmplem1  23559  kqnrmlem1  23661  kqnrmlem2  23662  nrmhmph  23712  fbssfi  23755  opnfbas  23760  fbasfip  23786  fbunfip  23787  fgss2  23792  fgcl  23796  supfil  23813  isufil2  23826  filssufilg  23829  ssufl  23836  ufileu  23837  elfm3  23868  fmfnfm  23876  ufldom  23880  fbflim2  23895  flfneii  23910  flftg  23914  txflf  23924  supnfcls  23938  fclscf  23943  fclsfnflim  23945  flimfnfcls  23946  alexsubALTlem2  23966  alexsubALTlem3  23967  alexsubALTlem4  23968  alexsubALT  23969  tsmsfbas  24046  tsmsres  24062  tsmsf1o  24063  tsmsxplem1  24071  tsmsxp  24073  ustssel  24124  ustincl  24126  ustdiag  24127  ustinvel  24128  ustexhalf  24129  ust0  24138  elutop  24151  ustuqtop4  24162  cfiluexsm  24207  cfiluweak  24212  blssps  24342  blss  24343  metss  24426  metrest  24442  metcnp3  24458  metnrmlem3  24780  lebnumlem3  24892  lebnum  24893  ellimc3  25810  lhop1lem  25948  dchrelbas  27177  eqscut2  27750  scutun12  27754  madebdayim  27836  madebday  27848  onsiso  28208  bdayn0p1  28297  upgredgpr  29124  dfnbgr3  29320  nbupgr  29326  nbumgrvtx  29328  nbgr2vtx1edg  29332  nbuhgr2vtx1edgb  29334  cusgrexilem2  29424  wlkvtxiedg  29607  wlkres  29651  upgr1wlkdlem2  30130  1pthon2v  30137  1pthon2ve  30138  cusconngr  30175  isfrgr  30244  avril1  30447  spanval  31317  spancl  31320  shsval2i  31371  omlsi  31388  ococin  31392  chsupsn  31397  pjoml  31420  shs00i  31434  chj00i  31471  chsscon3  31484  chlejb1  31496  chnle  31498  pjoml2  31595  pjoml3  31596  lecm  31601  stcltr1i  32258  mdbr  32278  dmdmd  32284  dmdi  32286  dmdbr3  32289  dmdbr4  32290  mdsl1i  32305  mdslmd1lem3  32311  mdslmd1lem4  32312  csmdsymi  32318  hatomic  32344  chrelat2  32354  atord  32372  atcvat4i  32381  fz1nntr  32791  elrgspnlem4  33221  fldgenval  33287  fldgensdrg  33289  fldgenssv  33290  fldgenssp  33293  nsgmgc  33386  nsgqusf1olem2  33388  isprmidl  33412  ssdifidllem  33430  ssdifidl  33431  ssdifidlprm  33432  mxidlmax  33439  ssmxidllem  33447  ssmxidl  33448  1arithufdlem4  33521  reff  33875  cmpcref  33886  zarcls1  33905  zarclsiin  33907  zarclssn  33909  zart0  33915  zarmxt1  33916  zarcmp  33918  rhmpreimacnlem  33920  sigagenval  34176  dmsigagen  34180  sigagenss  34185  ldsysgenld  34196  ldgenpisyslem1  34199  ldgenpisyslem2  34200  dynkin  34203  carsgmon  34350  carsgclctunlem2  34355  bnj1286  35054  bnj1452  35087  tz9.1regs  35153  fineqvac  35162  onvf1odlem4  35173  vonf1owev  35175  kur14lem9  35281  mclsssvlem  35629  mclsind  35637  imagesset  36020  altopthsn  36028  fnessref  36424  refssfne  36425  topjoin  36432  neifg  36438  bj-snglex  37040  bj-imdirvallem  37247  relowlssretop  37430  relowlpssretop  37431  exrecfnlem  37446  finxpreclem3  37460  pibt2  37484  poimirlem29  37712  poimir  37716  mblfinlem3  37722  totbndss  37840  heibor1lem  37872  unichnidl  38094  ispridl  38097  maxidlmax  38106  igenval  38124  igenidl  38126  igenmin  38127  igenval2  38129  dfsuccl4  38510  brssr  38616  lsatcmp  39125  lcvexchlem4  39159  lcvexchlem5  39160  pclvalN  40012  pclclN  40013  elpcliN  40015  docaclN  41246  dihglb2  41464  doch2val2  41486  dochocss  41488  dochexmidlem7  41588  lpolconN  41609  mapdval  41750  nacsfix  42832  mzpcompact2  42872  superficl  43687  superuncl  43688  cleq2lem  43728  clcnvlem  43743  dfrtrcl3  43853  clsk1indlem2  44162  neik0pk1imk0  44167  isotone1  44168  isotone2  44169  ntrclsiso  44187  gneispacess2  44266  mnuunid  44397  mnurndlem2  44402  ssrecnpr  44428  founiiun  45303  founiiun0  45314  islptre  45746  salgenval  46446  salgenn0  46456  salgencl  46457  sssalgen  46460  salgenss  46461  salgenuni  46462  issalgend  46463  dfsalgen2  46466  salgencntex  46468  dfclnbgr3  47953  predgclnbgrel  47966  clnbgredg  47967  clnbgrgrimlem  48060  clnbgrgrim  48061  opndisj  49030  opnneilem  49033  sepfsepc  49055  iscnrm3rlem8  49074  iscnrm3llem2  49077  intubeu  49111  ipolubdm  49114  ipoglbdm  49117  setrec1lem1  49815  setrec1lem3  49817  setrec2fun  49820