Theorem sseq2 3939

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 3928	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3920	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 33	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3920	. . . 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 3900

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  sseq12  3940  sseq2i  3942  sseq2d  3945  nssne1  3975  psseq2  4021  sseq0b  4356  un00  4360  disjpss  4417  pweqALT  4575  ssintab  4928  ssintub  4929  intmin  4931  treq  5223  al0ssb  5266  sseliALT  5267  ssexgOLD  5290  intabs  5315  iunopeqop  5499  iunopeqopOLD  5500  onelssex  6433  ordunidif  6434  ordssun  6488  fununi  6640  feq3  6714  ssimaexg  6997  fnssintima  7398  iunpw  7812  tfindsg  7899  limomss  7909  findsg  7936  funcnvuni  7971  frxp  8168  frrlem1  8335  frrlem13  8347  onfununi  8380  oawordeu  8594  oawordexr  8595  nnawordex  8677  eldifsucnn  8704  coflton  8711  cofon1  8712  cofon2  8713  cofonr  8714  naddcllem  8716  naddunif  8734  ereq1  8756  xpider  8840  domeng  9020  sbthlem4  9140  sbthlem5  9141  domssex  9188  ssfi  9219  finsschain  9379  dffi2  9445  dffi3  9453  hartogslem1  9566  inf3lema  9655  cantnflem1  9720  dfttrcl2  9755  tz9.1  9760  tz9.1c  9761  tctr  9769  tcmin  9770  tcrank  9931  scottex  9963  scottexOLD  9964  setrec1lem1  9996  setrec1lem3  9999  setrec2fun  10003  cardlim  10083  infxpenlem  10122  infxpenc2  10131  isinfcard  10201  alephinit  10204  alephval3  10219  dfac3  10230  cflem  10353  cfval  10354  cflecard  10360  cfsuc  10365  cff1  10366  cfflb  10367  cflim2  10371  isf32lem2  10462  fin1a2lem13  10520  ac7g  10582  ttukeylem5  10621  ttukeylem7  10623  pwcfsdom  10698  pwfseqlem5  10778  pwfseq  10779  gch2  10790  winalim  10810  wunex  10854  wuncss  10860  eltskg  10865  eltsk2g  10866  gruina  10933  grur1a  10934  axgroth6  10943  swrdnd2  14836  trcleq2lem  15176  dfrtrcl2  15247  fprodss  16147  mrcflem  17812  mrcval  17816  isacs2  17859  acsfiel  17860  ipoval  18736  fpwipodrs  18746  ipodrsima  18747  mreclatBAD  18769  slwispgp  19858  pgpssslw  19861  lsmss1b  19913  lsmss2b  19915  cntzcmnss  20088  gsumzres  20156  rgspnval  20897  rgspncl  20898  rgspnmin  20900  lspf  21282  lspval  21283  lbsextlem1  21469  lbsextlem3  21471  lbsextlem4  21472  unichnlidl  21549  rspprop  21557  isprmidl  21652  ssdifidllem  21673  ssdifidl  21674  ssdifidlprm  21675  aspval  22213  mplsubglem  22339  mpllsslem  22340  basis2  23302  eltg2  23309  clsval  23388  clscld  23398  clsval2  23401  ntrcls0  23427  isnei  23454  neiint  23455  neips  23464  opnneissb  23465  opnssneib  23466  neindisj2  23474  innei  23476  neiptoptop  23482  neiptopnei  23483  neitr  23531  restcls  23532  cnpimaex  23607  cnprest2  23641  regsep  23685  nrmsep3  23706  nrmsep  23708  regsep2  23727  tgcmp  23752  uncmp  23754  bwth  23761  1stcfb  23796  1stcrest  23804  2ndcctbss  23807  1stcelcls  23813  lly1stc  23848  ssref  23864  refref  23865  comppfsc  23884  xkoopn  23941  neitx  23959  txcnp  23972  txcmplem1  23993  kqnrmlem1  24095  kqnrmlem2  24096  nrmhmph  24146  fbssfi  24189  opnfbas  24194  fbasfip  24220  fbunfip  24221  fgss2  24226  fgcl  24230  supfil  24247  isufil2  24260  filssufilg  24263  ssufl  24270  ufileu  24271  elfm3  24302  fmfnfm  24310  ufldom  24314  fbflim2  24329  flfneii  24344  flftg  24348  txflf  24358  supnfcls  24372  fclscf  24377  fclsfnflim  24379  flimfnfcls  24380  alexsubALTlem2  24400  alexsubALTlem3  24401  alexsubALTlem4  24402  alexsubALT  24403  tsmsfbas  24480  tsmsres  24496  tsmsf1o  24497  tsmsxplem1  24505  tsmsxp  24507  ustssel  24558  ustincl  24560  ustdiag  24561  ustinvel  24562  ustexhalf  24563  ust0  24572  elutop  24585  ustuqtop4  24596  cfiluexsm  24641  cfiluweak  24646  blssps  24776  blss  24777  metss  24860  metrest  24876  metcnp3  24892  metnrmlem3  25214  lebnumlem3  25317  lebnum  25318  ellimc3  26232  lhop1lem  26366  dchrelbas  27596  eqcuts2  28205  cutsun12  28209  madebdayim  28307  madebday  28319  oniso  28690  bdayn0p1  28788  prlngd  29450  dfprlng2  29458  upgredgpr  29753  dfnbgr3  29952  nbupgr  29958  nbumgrvtx  29960  nbgr2vtx1edg  29964  nbuhgr2vtx1edgb  29966  cusgrexilem2  30056  wlkvtxiedg  30238  wlkres  30282  upgr1wlkdlem2  30770  1pthon2v  30787  1pthon2ve  30788  cusconngr  30825  isfrgr  30894  avril1  31097  spanval  31968  spancl  31971  shsval2i  32022  omlsi  32039  ococin  32043  chsupsn  32048  pjoml  32071  shs00i  32085  chj00i  32122  chsscon3  32135  chlejb1  32147  chnle  32149  pjoml2  32246  pjoml3  32247  lecm  32252  stcltr1i  32909  mdbr  32929  dmdmd  32935  dmdi  32937  dmdbr3  32940  dmdbr4  32941  mdsl1i  32956  mdslmd1lem3  32962  mdslmd1lem4  32963  csmdsymi  32969  hatomic  32995  chrelat2  33005  atord  33023  atcvat4i  33032  fz1nntr  33467  elrgspnlem4  33882  fldgenval  33958  fldgensdrg  33960  fldgenssv  33961  fldgenssp  33964  nsgmgc  34047  nsgqusf1olem2  34049  mxidlmax  34074  ssmxidllem  34082  ssmxidl  34083  dflringlem  34110  1arithufdlem4  34163  reff  34554  cmpcref  34565  zarcls1  34584  zarclsiin  34586  zarclssn  34588  zart0  34594  zarmxt1  34595  zarcmp  34597  rhmpreimacnlem  34599  sigagenval  34856  dmsigagen  34860  sigagenss  34865  ldsysgenld  34876  ldgenpisyslem1  34879  ldgenpisyslem2  34880  dynkin  34883  carsgmon  35029  carsgclctunlem2  35034  bnj1286  35732  bnj1452  35765  rankse  35836  fineqvac  35897  tz9.1regs  35915  onvf1odlem4  36047  vonf1wev  36049  vonf1owevOLD  36051  kur14lem9  36159  mclsssvlem  36507  mclsind  36515  imagesset  36908  altopthsn  36917  fnessref  37336  refssfne  37337  topjoin  37344  neifg  37350  tz9.1tco  37462  ttc00  37487  dfttc3gw  37502  bj-snglex  38077  bj-imdirvallem  38306  relowlssretop  38491  relowlpssretop  38492  exrecfnlem  38507  finxpreclem3  38521  pibt2  38545  poimirlem29  38772  poimir  38776  mblfinlem3  38782  totbndss  38914  heibor1lem  38946  unichnidl  39168  ispridl  39171  maxidlmax  39180  igenval  39198  igenidl  39200  igenmin  39201  igenval2  39203  dfsuccl4  39609  brssr  39716  suceldisj  39953  lsatcmp  40263  lcvexchlem4  40297  lcvexchlem5  40298  pclvalN  41150  pclclN  41151  elpcliN  41153  docaclN  42384  dihglb2  42602  doch2val2  42624  dochocss  42626  dochexmidlem7  42726  lpolconN  42747  mapdval  42888  nacsfix  43927  mzpcompact2  43967  superficl  44771  superuncl  44772  cleq2lem  44811  clcnvlem  44826  dfrtrcl3  44936  clsk1indlem2  45245  neik0pk1imk0  45250  isotone1  45251  isotone2  45252  ntrclsiso  45270  gneispacess2  45349  mnuunid  45464  mnurndlem2  45469  ssrecnpr  45495  founiiun  46409  founiiun0  46420  islptre  46846  salgenval  47546  salgenn0  47556  salgencl  47557  sssalgen  47560  salgenss  47561  salgenuni  47562  issalgend  47563  dfsalgen2  47566  salgencntex  47568  dfclnbgr3  49139  predgclnbgrel  49152  clnbgredg  49153  clnbgrgrimlem  49246  clnbgrgrim  49247  opndisj  50232  opnneilem  50235  sepfsepc  50257  iscnrm3rlem8  50276  iscnrm3llem2  50279  intubeu  50313  ipolubdm  50316  ipoglbdm  50319