Theorem sseq2 3961

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 3950	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3941	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3941	. . . 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 3902

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 2121  ax-ext 2703

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

This theorem is referenced by:  sseq12  3962  sseq2i  3964  sseq2d  3967  nssne1  3997  psseq2  4041  sseq0  4353  un00  4395  disjpss  4411  pweqALT  4565  ssintab  4915  ssintub  4916  intmin  4918  treq  5205  al0ssb  5246  sseliALT  5247  ssexg  5261  intabs  5287  iunopeqop  5461  onelssex  6355  ordunidif  6356  ordssun  6410  fununi  6556  feq3  6631  ssimaexg  6908  fnssintima  7296  iunpw  7704  tfindsg  7791  limomss  7801  findsg  7827  funcnvuni  7862  frxp  8056  frrlem1  8216  frrlem13  8228  onfununi  8261  oawordeu  8470  oawordexr  8471  nnawordex  8552  eldifsucnn  8579  coflton  8586  cofon1  8587  cofon2  8588  cofonr  8589  naddcllem  8591  naddunif  8608  ereq1  8629  xpider  8712  domeng  8885  sbthlem4  9003  sbthlem5  9004  domssex  9051  ssfi  9082  finsschain  9243  dffi2  9307  dffi3  9315  hartogslem1  9428  inf3lema  9514  cantnflem1  9579  dfttrcl2  9614  tz9.1  9619  tz9.1c  9620  tctr  9628  tcmin  9629  tcrank  9777  scottex  9778  cardlim  9865  infxpenlem  9904  infxpenc2  9913  isinfcard  9983  alephinit  9986  alephval3  10001  dfac3  10012  cflem  10136  cflemOLD  10137  cfval  10138  cflecard  10144  cfsuc  10148  cff1  10149  cfflb  10150  cflim2  10154  isf32lem2  10245  fin1a2lem13  10303  ac7g  10365  ttukeylem5  10404  ttukeylem7  10406  pwcfsdom  10474  pwfseqlem5  10554  pwfseq  10555  gch2  10566  winalim  10586  wunex  10630  wuncss  10636  eltskg  10641  eltsk2g  10642  gruina  10709  grur1a  10710  axgroth6  10719  swrdnd2  14563  trcleq2lem  14898  dfrtrcl2  14969  fprodss  15855  mrcflem  17512  mrcval  17516  isacs2  17559  acsfiel  17560  ipoval  18436  fpwipodrs  18446  ipodrsima  18447  mreclatBAD  18469  slwispgp  19524  pgpssslw  19527  lsmss1b  19579  lsmss2b  19581  cntzcmnss  19754  gsumzres  19822  rgspnval  20528  rgspncl  20529  rgspnmin  20531  lspf  20908  lspval  20909  lbsextlem1  21096  lbsextlem3  21098  lbsextlem4  21099  aspval  21811  mplsubglem  21937  mpllsslem  21938  basis2  22867  eltg2  22874  clsval  22953  clscld  22963  clsval2  22966  ntrcls0  22992  isnei  23019  neiint  23020  neips  23029  opnneissb  23030  opnssneib  23031  neindisj2  23039  innei  23041  neiptoptop  23047  neiptopnei  23048  neitr  23096  restcls  23097  cnpimaex  23172  cnprest2  23206  regsep  23250  nrmsep3  23271  nrmsep  23273  regsep2  23292  tgcmp  23317  uncmp  23319  bwth  23326  1stcfb  23361  1stcrest  23369  2ndcctbss  23371  1stcelcls  23377  lly1stc  23412  ssref  23428  refref  23429  comppfsc  23448  xkoopn  23505  neitx  23523  txcnp  23536  txcmplem1  23557  kqnrmlem1  23659  kqnrmlem2  23660  nrmhmph  23710  fbssfi  23753  opnfbas  23758  fbasfip  23784  fbunfip  23785  fgss2  23790  fgcl  23794  supfil  23811  isufil2  23824  filssufilg  23827  ssufl  23834  ufileu  23835  elfm3  23866  fmfnfm  23874  ufldom  23878  fbflim2  23893  flfneii  23908  flftg  23912  txflf  23922  supnfcls  23936  fclscf  23941  fclsfnflim  23943  flimfnfcls  23944  alexsubALTlem2  23964  alexsubALTlem3  23965  alexsubALTlem4  23966  alexsubALT  23967  tsmsfbas  24044  tsmsres  24060  tsmsf1o  24061  tsmsxplem1  24069  tsmsxp  24071  ustssel  24122  ustincl  24124  ustdiag  24125  ustinvel  24126  ustexhalf  24127  ust0  24136  elutop  24149  ustuqtop4  24160  cfiluexsm  24205  cfiluweak  24210  blssps  24340  blss  24341  metss  24424  metrest  24440  metcnp3  24456  metnrmlem3  24778  lebnumlem3  24890  lebnum  24891  ellimc3  25808  lhop1lem  25946  dchrelbas  27175  eqscut2  27748  scutun12  27752  madebdayim  27834  madebday  27846  onsiso  28206  bdayn0p1  28295  upgredgpr  29121  dfnbgr3  29317  nbupgr  29323  nbumgrvtx  29325  nbgr2vtx1edg  29329  nbuhgr2vtx1edgb  29331  cusgrexilem2  29421  wlkvtxiedg  29604  wlkres  29648  upgr1wlkdlem2  30124  1pthon2v  30131  1pthon2ve  30132  cusconngr  30169  isfrgr  30238  avril1  30441  spanval  31311  spancl  31314  shsval2i  31365  omlsi  31382  ococin  31386  chsupsn  31391  pjoml  31414  shs00i  31428  chj00i  31465  chsscon3  31478  chlejb1  31490  chnle  31492  pjoml2  31589  pjoml3  31590  lecm  31595  stcltr1i  32252  mdbr  32272  dmdmd  32278  dmdi  32280  dmdbr3  32283  dmdbr4  32284  mdsl1i  32299  mdslmd1lem3  32305  mdslmd1lem4  32306  csmdsymi  32312  hatomic  32338  chrelat2  32348  atord  32366  atcvat4i  32375  fz1nntr  32782  elrgspnlem4  33210  fldgenval  33276  fldgensdrg  33278  fldgenssv  33279  fldgenssp  33282  nsgmgc  33375  nsgqusf1olem2  33377  isprmidl  33401  ssdifidllem  33419  ssdifidl  33420  ssdifidlprm  33421  mxidlmax  33428  ssmxidllem  33436  ssmxidl  33437  1arithufdlem4  33510  reff  33850  cmpcref  33861  zarcls1  33880  zarclsiin  33882  zarclssn  33884  zart0  33890  zarmxt1  33891  zarcmp  33893  rhmpreimacnlem  33895  sigagenval  34151  dmsigagen  34155  sigagenss  34160  ldsysgenld  34171  ldgenpisyslem1  34174  ldgenpisyslem2  34175  dynkin  34178  carsgmon  34325  carsgclctunlem2  34330  bnj1286  35029  bnj1452  35062  tz9.1regs  35128  fineqvac  35137  onvf1odlem4  35148  vonf1owev  35150  kur14lem9  35256  mclsssvlem  35604  mclsind  35612  imagesset  35993  altopthsn  36001  fnessref  36397  refssfne  36398  topjoin  36405  neifg  36411  bj-snglex  37013  bj-imdirvallem  37220  relowlssretop  37403  relowlpssretop  37404  exrecfnlem  37419  finxpreclem3  37433  pibt2  37457  poimirlem29  37695  poimir  37699  mblfinlem3  37705  totbndss  37823  heibor1lem  37855  unichnidl  38077  ispridl  38080  maxidlmax  38089  igenval  38107  igenidl  38109  igenmin  38110  igenval2  38112  brssr  38544  lsatcmp  39048  lcvexchlem4  39082  lcvexchlem5  39083  pclvalN  39935  pclclN  39936  elpcliN  39938  docaclN  41169  dihglb2  41387  doch2val2  41409  dochocss  41411  dochexmidlem7  41511  lpolconN  41532  mapdval  41673  nacsfix  42751  mzpcompact2  42791  superficl  43606  superuncl  43607  cleq2lem  43647  clcnvlem  43662  dfrtrcl3  43772  clsk1indlem2  44081  neik0pk1imk0  44086  isotone1  44087  isotone2  44088  ntrclsiso  44106  gneispacess2  44185  mnuunid  44316  mnurndlem2  44321  ssrecnpr  44347  founiiun  45222  founiiun0  45233  islptre  45665  salgenval  46365  salgenn0  46375  salgencl  46376  sssalgen  46379  salgenss  46380  salgenuni  46381  issalgend  46382  dfsalgen2  46385  salgencntex  46387  dfclnbgr3  47863  predgclnbgrel  47876  clnbgredg  47877  clnbgrgrimlem  47970  clnbgrgrim  47971  opndisj  48940  opnneilem  48943  sepfsepc  48965  iscnrm3rlem8  48984  iscnrm3llem2  48987  intubeu  49021  ipolubdm  49024  ipoglbdm  49027  setrec1lem1  49725  setrec1lem3  49727  setrec2fun  49730