Theorem sseq2 3990

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 3979	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3970	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
3	2	com12 32	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
4		sstr2 3970	. . . 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 1540   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-ss 3948

This theorem is referenced by:  sseq12  3991  sseq2i  3993  sseq2d  3996  nssne1  4026  psseq2  4071  sseq0  4383  un00  4425  disjpss  4441  pweqALT  4595  ssintab  4946  ssintub  4947  intmin  4949  treq  5242  al0ssb  5283  sseliALT  5284  ssexg  5298  intabs  5324  iunopeqop  5501  onelssex  6406  ordunidif  6407  ordssun  6461  fununi  6616  feq3  6693  ssimaexg  6970  fnssintima  7360  iunpw  7770  tfindsg  7861  limomss  7871  findsg  7898  funcnvuni  7933  frxp  8130  frrlem1  8290  frrlem13  8302  wrecseq123OLD  8319  wfrlem1OLD  8327  wfrlem4OLD  8331  wfrlem15OLD  8342  onfununi  8360  oawordeu  8572  oawordexr  8573  nnawordex  8654  eldifsucnn  8681  coflton  8688  cofon1  8689  cofon2  8690  cofonr  8691  naddcllem  8693  naddunif  8710  ereq1  8731  xpider  8807  domeng  8982  sbthlem4  9105  sbthlem5  9106  domssex  9157  ssfi  9192  finsschain  9376  dffi2  9440  dffi3  9448  hartogslem1  9561  inf3lema  9643  cantnflem1  9708  dfttrcl2  9743  tz9.1  9748  tz9.1c  9749  tctr  9759  tcmin  9760  tcrank  9903  scottex  9904  cardlim  9991  infxpenlem  10032  infxpenc2  10041  isinfcard  10111  alephinit  10114  alephval3  10129  dfac3  10140  cflem  10264  cflemOLD  10265  cfval  10266  cflecard  10272  cfsuc  10276  cff1  10277  cfflb  10278  cflim2  10282  isf32lem2  10373  fin1a2lem13  10431  ac7g  10493  ttukeylem5  10532  ttukeylem7  10534  pwcfsdom  10602  pwfseqlem5  10682  pwfseq  10683  gch2  10694  winalim  10714  wunex  10758  wuncss  10764  eltskg  10769  eltsk2g  10770  gruina  10837  grur1a  10838  axgroth6  10847  swrdnd2  14678  trcleq2lem  15015  dfrtrcl2  15086  fprodss  15969  mrcflem  17623  mrcval  17627  isacs2  17670  acsfiel  17671  ipoval  18545  fpwipodrs  18555  ipodrsima  18556  mreclatBAD  18578  slwispgp  19597  pgpssslw  19600  lsmss1b  19652  lsmss2b  19654  cntzcmnss  19827  gsumzres  19895  rgspnval  20577  rgspncl  20578  rgspnmin  20580  lspf  20936  lspval  20937  lbsextlem1  21124  lbsextlem3  21126  lbsextlem4  21127  aspval  21838  mplsubglem  21964  mpllsslem  21965  basis2  22894  eltg2  22901  clsval  22980  clscld  22990  clsval2  22993  ntrcls0  23019  isnei  23046  neiint  23047  neips  23056  opnneissb  23057  opnssneib  23058  neindisj2  23066  innei  23068  neiptoptop  23074  neiptopnei  23075  neitr  23123  restcls  23124  cnpimaex  23199  cnprest2  23233  regsep  23277  nrmsep3  23298  nrmsep  23300  regsep2  23319  tgcmp  23344  uncmp  23346  bwth  23353  1stcfb  23388  1stcrest  23396  2ndcctbss  23398  1stcelcls  23404  lly1stc  23439  ssref  23455  refref  23456  comppfsc  23475  xkoopn  23532  neitx  23550  txcnp  23563  txcmplem1  23584  kqnrmlem1  23686  kqnrmlem2  23687  nrmhmph  23737  fbssfi  23780  opnfbas  23785  fbasfip  23811  fbunfip  23812  fgss2  23817  fgcl  23821  supfil  23838  isufil2  23851  filssufilg  23854  ssufl  23861  ufileu  23862  elfm3  23893  fmfnfm  23901  ufldom  23905  fbflim2  23920  flfneii  23935  flftg  23939  txflf  23949  supnfcls  23963  fclscf  23968  fclsfnflim  23970  flimfnfcls  23971  alexsubALTlem2  23991  alexsubALTlem3  23992  alexsubALTlem4  23993  alexsubALT  23994  tsmsfbas  24071  tsmsres  24087  tsmsf1o  24088  tsmsxplem1  24096  tsmsxp  24098  ustssel  24149  ustincl  24151  ustdiag  24152  ustinvel  24153  ustexhalf  24154  ust0  24163  elutop  24177  ustuqtop4  24188  cfiluexsm  24233  cfiluweak  24238  blssps  24368  blss  24369  metss  24452  metrest  24468  metcnp3  24484  metnrmlem3  24806  lebnumlem3  24918  lebnum  24919  ellimc3  25837  lhop1lem  25975  dchrelbas  27204  eqscut2  27775  scutun12  27779  madebdayim  27856  madebday  27868  onsiso  28226  bdayn0p1  28315  upgredgpr  29126  dfnbgr3  29322  nbupgr  29328  nbumgrvtx  29330  nbgr2vtx1edg  29334  nbuhgr2vtx1edgb  29336  cusgrexilem2  29426  wlkvtxiedg  29610  wlkres  29655  upgr1wlkdlem2  30132  1pthon2v  30139  1pthon2ve  30140  cusconngr  30177  isfrgr  30246  avril1  30449  spanval  31319  spancl  31322  shsval2i  31373  omlsi  31390  ococin  31394  chsupsn  31399  pjoml  31422  shs00i  31436  chj00i  31473  chsscon3  31486  chlejb1  31498  chnle  31500  pjoml2  31597  pjoml3  31598  lecm  31603  stcltr1i  32260  mdbr  32280  dmdmd  32286  dmdi  32288  dmdbr3  32291  dmdbr4  32292  mdsl1i  32307  mdslmd1lem3  32313  mdslmd1lem4  32314  csmdsymi  32320  hatomic  32346  chrelat2  32356  atord  32374  atcvat4i  32383  fz1nntr  32786  elrgspnlem4  33245  fldgenval  33311  fldgensdrg  33313  fldgenssv  33314  fldgenssp  33317  nsgmgc  33432  nsgqusf1olem2  33434  isprmidl  33458  ssdifidllem  33476  ssdifidl  33477  ssdifidlprm  33478  mxidlmax  33485  ssmxidllem  33493  ssmxidl  33494  1arithufdlem4  33567  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  34351  carsgclctunlem2  34356  bnj1286  35055  bnj1452  35088  fineqvac  35133  kur14lem9  35241  mclsssvlem  35589  mclsind  35597  imagesset  35976  altopthsn  35984  fnessref  36380  refssfne  36381  topjoin  36388  neifg  36394  bj-snglex  36996  bj-imdirvallem  37203  relowlssretop  37386  relowlpssretop  37387  exrecfnlem  37402  finxpreclem3  37416  pibt2  37440  poimirlem29  37678  poimir  37682  mblfinlem3  37688  totbndss  37806  heibor1lem  37838  unichnidl  38060  ispridl  38063  maxidlmax  38072  igenval  38090  igenidl  38092  igenmin  38093  igenval2  38095  brssr  38524  lsatcmp  39026  lcvexchlem4  39060  lcvexchlem5  39061  pclvalN  39914  pclclN  39915  elpcliN  39917  docaclN  41148  dihglb2  41366  doch2val2  41388  dochocss  41390  dochexmidlem7  41490  lpolconN  41511  mapdval  41652  nacsfix  42710  mzpcompact2  42750  superficl  43566  superuncl  43567  cleq2lem  43607  clcnvlem  43622  dfrtrcl3  43732  clsk1indlem2  44041  neik0pk1imk0  44046  isotone1  44047  isotone2  44048  ntrclsiso  44066  gneispacess2  44145  mnuunid  44276  mnurndlem2  44281  ssrecnpr  44307  founiiun  45183  founiiun0  45194  islptre  45628  salgenval  46330  salgenn0  46340  salgencl  46341  sssalgen  46344  salgenss  46345  salgenuni  46346  issalgend  46347  dfsalgen2  46350  salgencntex  46352  dfclnbgr3  47820  predgclnbgrel  47832  clnbgredg  47833  clnbgrgrimlem  47926  clnbgrgrim  47927  opndisj  48857  opnneilem  48860  sepfsepc  48882  iscnrm3rlem8  48901  iscnrm3llem2  48904  intubeu  48938  ipolubdm  48941  ipoglbdm  48944  setrec1lem1  49531  setrec1lem3  49533  setrec2fun  49536