Theorem sseq2 3960

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

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 2708

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

This theorem is referenced by:  sseq12  3961  sseq2i  3963  sseq2d  3966  nssne1  3996  psseq2  4043  sseq0  4355  un00  4397  disjpss  4413  pweqALT  4569  ssintab  4920  ssintub  4921  intmin  4923  treq  5212  al0ssb  5253  sseliALT  5254  ssexg  5268  intabs  5294  iunopeqop  5469  onelssex  6366  ordunidif  6367  ordssun  6421  fununi  6567  feq3  6642  ssimaexg  6920  fnssintima  7308  iunpw  7716  tfindsg  7803  limomss  7813  findsg  7839  funcnvuni  7874  frxp  8068  frrlem1  8228  frrlem13  8240  onfununi  8273  oawordeu  8482  oawordexr  8483  nnawordex  8565  eldifsucnn  8592  coflton  8599  cofon1  8600  cofon2  8601  cofonr  8602  naddcllem  8604  naddunif  8621  ereq1  8642  xpider  8725  domeng  8899  sbthlem4  9018  sbthlem5  9019  domssex  9066  ssfi  9097  finsschain  9259  dffi2  9326  dffi3  9334  hartogslem1  9447  inf3lema  9533  cantnflem1  9598  dfttrcl2  9633  tz9.1  9638  tz9.1c  9639  tctr  9647  tcmin  9648  tcrank  9796  scottex  9797  cardlim  9884  infxpenlem  9923  infxpenc2  9932  isinfcard  10002  alephinit  10005  alephval3  10020  dfac3  10031  cflem  10155  cflemOLD  10156  cfval  10157  cflecard  10163  cfsuc  10167  cff1  10168  cfflb  10169  cflim2  10173  isf32lem2  10264  fin1a2lem13  10322  ac7g  10384  ttukeylem5  10423  ttukeylem7  10425  pwcfsdom  10494  pwfseqlem5  10574  pwfseq  10575  gch2  10586  winalim  10606  wunex  10650  wuncss  10656  eltskg  10661  eltsk2g  10662  gruina  10729  grur1a  10730  axgroth6  10739  swrdnd2  14579  trcleq2lem  14914  dfrtrcl2  14985  fprodss  15871  mrcflem  17529  mrcval  17533  isacs2  17576  acsfiel  17577  ipoval  18453  fpwipodrs  18463  ipodrsima  18464  mreclatBAD  18486  slwispgp  19540  pgpssslw  19543  lsmss1b  19595  lsmss2b  19597  cntzcmnss  19770  gsumzres  19838  rgspnval  20545  rgspncl  20546  rgspnmin  20548  lspf  20925  lspval  20926  lbsextlem1  21113  lbsextlem3  21115  lbsextlem4  21116  aspval  21828  mplsubglem  21954  mpllsslem  21955  basis2  22895  eltg2  22902  clsval  22981  clscld  22991  clsval2  22994  ntrcls0  23020  isnei  23047  neiint  23048  neips  23057  opnneissb  23058  opnssneib  23059  neindisj2  23067  innei  23069  neiptoptop  23075  neiptopnei  23076  neitr  23124  restcls  23125  cnpimaex  23200  cnprest2  23234  regsep  23278  nrmsep3  23299  nrmsep  23301  regsep2  23320  tgcmp  23345  uncmp  23347  bwth  23354  1stcfb  23389  1stcrest  23397  2ndcctbss  23399  1stcelcls  23405  lly1stc  23440  ssref  23456  refref  23457  comppfsc  23476  xkoopn  23533  neitx  23551  txcnp  23564  txcmplem1  23585  kqnrmlem1  23687  kqnrmlem2  23688  nrmhmph  23738  fbssfi  23781  opnfbas  23786  fbasfip  23812  fbunfip  23813  fgss2  23818  fgcl  23822  supfil  23839  isufil2  23852  filssufilg  23855  ssufl  23862  ufileu  23863  elfm3  23894  fmfnfm  23902  ufldom  23906  fbflim2  23921  flfneii  23936  flftg  23940  txflf  23950  supnfcls  23964  fclscf  23969  fclsfnflim  23971  flimfnfcls  23972  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALTlem4  23994  alexsubALT  23995  tsmsfbas  24072  tsmsres  24088  tsmsf1o  24089  tsmsxplem1  24097  tsmsxp  24099  ustssel  24150  ustincl  24152  ustdiag  24153  ustinvel  24154  ustexhalf  24155  ust0  24164  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  25836  lhop1lem  25974  dchrelbas  27203  eqcuts2  27782  cutsun12  27786  madebdayim  27884  madebday  27896  oniso  28267  bdayn0p1  28365  upgredgpr  29215  dfnbgr3  29411  nbupgr  29417  nbumgrvtx  29419  nbgr2vtx1edg  29423  nbuhgr2vtx1edgb  29425  cusgrexilem2  29515  wlkvtxiedg  29698  wlkres  29742  upgr1wlkdlem2  30221  1pthon2v  30228  1pthon2ve  30229  cusconngr  30266  isfrgr  30335  avril1  30538  spanval  31408  spancl  31411  shsval2i  31462  omlsi  31479  ococin  31483  chsupsn  31488  pjoml  31511  shs00i  31525  chj00i  31562  chsscon3  31575  chlejb1  31587  chnle  31589  pjoml2  31686  pjoml3  31687  lecm  31692  stcltr1i  32349  mdbr  32369  dmdmd  32375  dmdi  32377  dmdbr3  32380  dmdbr4  32381  mdsl1i  32396  mdslmd1lem3  32402  mdslmd1lem4  32403  csmdsymi  32409  hatomic  32435  chrelat2  32445  atord  32463  atcvat4i  32472  fz1nntr  32882  elrgspnlem4  33327  fldgenval  33394  fldgensdrg  33396  fldgenssv  33397  fldgenssp  33400  nsgmgc  33493  nsgqusf1olem2  33495  isprmidl  33519  ssdifidllem  33537  ssdifidl  33538  ssdifidlprm  33539  mxidlmax  33546  ssmxidllem  33554  ssmxidl  33555  1arithufdlem4  33628  reff  33996  cmpcref  34007  zarcls1  34026  zarclsiin  34028  zarclssn  34030  zart0  34036  zarmxt1  34037  zarcmp  34039  rhmpreimacnlem  34041  sigagenval  34297  dmsigagen  34301  sigagenss  34306  ldsysgenld  34317  ldgenpisyslem1  34320  ldgenpisyslem2  34321  dynkin  34324  carsgmon  34471  carsgclctunlem2  34476  bnj1286  35175  bnj1452  35208  fineqvac  35272  tz9.1regs  35290  onvf1odlem4  35300  vonf1owev  35302  kur14lem9  35408  mclsssvlem  35756  mclsind  35764  imagesset  36147  altopthsn  36155  fnessref  36551  refssfne  36552  topjoin  36559  neifg  36565  bj-snglex  37174  bj-imdirvallem  37385  relowlssretop  37568  relowlpssretop  37569  exrecfnlem  37584  finxpreclem3  37598  pibt2  37622  poimirlem29  37850  poimir  37854  mblfinlem3  37860  totbndss  37978  heibor1lem  38010  unichnidl  38232  ispridl  38235  maxidlmax  38244  igenval  38262  igenidl  38264  igenmin  38265  igenval2  38267  dfsuccl4  38648  brssr  38754  lsatcmp  39263  lcvexchlem4  39297  lcvexchlem5  39298  pclvalN  40150  pclclN  40151  elpcliN  40153  docaclN  41384  dihglb2  41602  doch2val2  41624  dochocss  41626  dochexmidlem7  41726  lpolconN  41747  mapdval  41888  nacsfix  42954  mzpcompact2  42994  superficl  43808  superuncl  43809  cleq2lem  43849  clcnvlem  43864  dfrtrcl3  43974  clsk1indlem2  44283  neik0pk1imk0  44288  isotone1  44289  isotone2  44290  ntrclsiso  44308  gneispacess2  44387  mnuunid  44518  mnurndlem2  44523  ssrecnpr  44549  founiiun  45423  founiiun0  45434  islptre  45865  salgenval  46565  salgenn0  46575  salgencl  46576  sssalgen  46579  salgenss  46580  salgenuni  46581  issalgend  46582  dfsalgen2  46585  salgencntex  46587  dfclnbgr3  48072  predgclnbgrel  48085  clnbgredg  48086  clnbgrgrimlem  48179  clnbgrgrim  48180  opndisj  49148  opnneilem  49151  sepfsepc  49173  iscnrm3rlem8  49192  iscnrm3llem2  49195  intubeu  49229  ipolubdm  49232  ipoglbdm  49235  setrec1lem1  49932  setrec1lem3  49934  setrec2fun  49937