Theorem sseq2 3948

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  sseq12  3949  sseq2i  3951  sseq2d  3954  nssne1  3984  psseq2  4029  sseq0  4338  un00  4380  disjpss  4396  pweqALT  4551  ssintab  4902  ssintub  4903  intmin  4905  treq  5193  al0ssb  5237  sseliALT  5238  ssexg  5258  intabs  5284  iunopeqop  5469  iunopeqopOLD  5470  onelssex  6366  ordunidif  6367  ordssun  6421  fununi  6567  feq3  6642  ssimaexg  6920  fnssintima  7313  iunpw  7721  tfindsg  7808  limomss  7818  findsg  7844  funcnvuni  7879  frxp  8073  frrlem1  8233  frrlem13  8245  onfununi  8278  oawordeu  8487  oawordexr  8488  nnawordex  8570  eldifsucnn  8597  coflton  8604  cofon1  8605  cofon2  8606  cofonr  8607  naddcllem  8609  naddunif  8626  ereq1  8648  xpider  8732  domeng  8906  sbthlem4  9025  sbthlem5  9026  domssex  9073  ssfi  9104  finsschain  9266  dffi2  9333  dffi3  9341  hartogslem1  9454  inf3lema  9543  cantnflem1  9608  dfttrcl2  9643  tz9.1  9648  tz9.1c  9649  tctr  9657  tcmin  9658  tcrank  9806  scottex  9807  cardlim  9894  infxpenlem  9933  infxpenc2  9942  isinfcard  10012  alephinit  10015  alephval3  10030  dfac3  10041  cflem  10165  cflemOLD  10166  cfval  10167  cflecard  10173  cfsuc  10177  cff1  10178  cfflb  10179  cflim2  10183  isf32lem2  10274  fin1a2lem13  10332  ac7g  10394  ttukeylem5  10433  ttukeylem7  10435  pwcfsdom  10504  pwfseqlem5  10584  pwfseq  10585  gch2  10596  winalim  10616  wunex  10660  wuncss  10666  eltskg  10671  eltsk2g  10672  gruina  10739  grur1a  10740  axgroth6  10749  swrdnd2  14616  trcleq2lem  14951  dfrtrcl2  15022  fprodss  15911  mrcflem  17570  mrcval  17574  isacs2  17617  acsfiel  17618  ipoval  18494  fpwipodrs  18504  ipodrsima  18505  mreclatBAD  18527  slwispgp  19584  pgpssslw  19587  lsmss1b  19639  lsmss2b  19641  cntzcmnss  19814  gsumzres  19882  rgspnval  20591  rgspncl  20592  rgspnmin  20594  lspf  20971  lspval  20972  lbsextlem1  21158  lbsextlem3  21160  lbsextlem4  21161  aspval  21854  mplsubglem  21980  mpllsslem  21981  basis2  22941  eltg2  22948  clsval  23027  clscld  23037  clsval2  23040  ntrcls0  23066  isnei  23093  neiint  23094  neips  23103  opnneissb  23104  opnssneib  23105  neindisj2  23113  innei  23115  neiptoptop  23121  neiptopnei  23122  neitr  23170  restcls  23171  cnpimaex  23246  cnprest2  23280  regsep  23324  nrmsep3  23345  nrmsep  23347  regsep2  23366  tgcmp  23391  uncmp  23393  bwth  23400  1stcfb  23435  1stcrest  23443  2ndcctbss  23445  1stcelcls  23451  lly1stc  23486  ssref  23502  refref  23503  comppfsc  23522  xkoopn  23579  neitx  23597  txcnp  23610  txcmplem1  23631  kqnrmlem1  23733  kqnrmlem2  23734  nrmhmph  23784  fbssfi  23827  opnfbas  23832  fbasfip  23858  fbunfip  23859  fgss2  23864  fgcl  23868  supfil  23885  isufil2  23898  filssufilg  23901  ssufl  23908  ufileu  23909  elfm3  23940  fmfnfm  23948  ufldom  23952  fbflim2  23967  flfneii  23982  flftg  23986  txflf  23996  supnfcls  24010  fclscf  24015  fclsfnflim  24017  flimfnfcls  24018  alexsubALTlem2  24038  alexsubALTlem3  24039  alexsubALTlem4  24040  alexsubALT  24041  tsmsfbas  24118  tsmsres  24134  tsmsf1o  24135  tsmsxplem1  24143  tsmsxp  24145  ustssel  24196  ustincl  24198  ustdiag  24199  ustinvel  24200  ustexhalf  24201  ust0  24210  elutop  24223  ustuqtop4  24234  cfiluexsm  24279  cfiluweak  24284  blssps  24414  blss  24415  metss  24498  metrest  24514  metcnp3  24530  metnrmlem3  24852  lebnumlem3  24955  lebnum  24956  ellimc3  25871  lhop1lem  26005  dchrelbas  27224  eqcuts2  27803  cutsun12  27807  madebdayim  27905  madebday  27917  oniso  28288  bdayn0p1  28386  upgredgpr  29236  dfnbgr3  29432  nbupgr  29438  nbumgrvtx  29440  nbgr2vtx1edg  29444  nbuhgr2vtx1edgb  29446  cusgrexilem2  29536  wlkvtxiedg  29718  wlkres  29762  upgr1wlkdlem2  30241  1pthon2v  30248  1pthon2ve  30249  cusconngr  30286  isfrgr  30355  avril1  30558  spanval  31429  spancl  31432  shsval2i  31483  omlsi  31500  ococin  31504  chsupsn  31509  pjoml  31532  shs00i  31546  chj00i  31583  chsscon3  31596  chlejb1  31608  chnle  31610  pjoml2  31707  pjoml3  31708  lecm  31713  stcltr1i  32370  mdbr  32390  dmdmd  32396  dmdi  32398  dmdbr3  32401  dmdbr4  32402  mdsl1i  32417  mdslmd1lem3  32423  mdslmd1lem4  32424  csmdsymi  32430  hatomic  32456  chrelat2  32466  atord  32484  atcvat4i  32493  fz1nntr  32901  elrgspnlem4  33333  fldgenval  33403  fldgensdrg  33405  fldgenssv  33406  fldgenssp  33409  nsgmgc  33502  nsgqusf1olem2  33504  isprmidl  33528  ssdifidllem  33546  ssdifidl  33547  ssdifidlprm  33548  mxidlmax  33555  ssmxidllem  33563  ssmxidl  33564  1arithufdlem4  33637  reff  34030  cmpcref  34041  zarcls1  34060  zarclsiin  34062  zarclssn  34064  zart0  34070  zarmxt1  34071  zarcmp  34073  rhmpreimacnlem  34075  sigagenval  34331  dmsigagen  34335  sigagenss  34340  ldsysgenld  34351  ldgenpisyslem1  34354  ldgenpisyslem2  34355  dynkin  34358  carsgmon  34505  carsgclctunlem2  34510  bnj1286  35208  bnj1452  35241  fineqvac  35304  tz9.1regs  35322  onvf1odlem4  35341  vonf1owev  35343  kur14lem9  35449  mclsssvlem  35797  mclsind  35805  imagesset  36188  altopthsn  36196  fnessref  36592  refssfne  36593  topjoin  36600  neifg  36606  tz9.1tco  36718  ttc00  36743  dfttc3gw  36758  bj-snglex  37333  bj-imdirvallem  37547  relowlssretop  37732  relowlpssretop  37733  exrecfnlem  37748  finxpreclem3  37762  pibt2  37786  poimirlem29  38023  poimir  38027  mblfinlem3  38033  totbndss  38151  heibor1lem  38183  unichnidl  38405  ispridl  38408  maxidlmax  38417  igenval  38435  igenidl  38437  igenmin  38438  igenval2  38440  dfsuccl4  38848  brssr  38955  suceldisj  39192  lsatcmp  39502  lcvexchlem4  39536  lcvexchlem5  39537  pclvalN  40389  pclclN  40390  elpcliN  40392  docaclN  41623  dihglb2  41841  doch2val2  41863  dochocss  41865  dochexmidlem7  41965  lpolconN  41986  mapdval  42127  nacsfix  43168  mzpcompact2  43208  superficl  44018  superuncl  44019  cleq2lem  44059  clcnvlem  44074  dfrtrcl3  44184  clsk1indlem2  44493  neik0pk1imk0  44498  isotone1  44499  isotone2  44500  ntrclsiso  44518  gneispacess2  44597  mnuunid  44728  mnurndlem2  44733  ssrecnpr  44759  founiiun  45633  founiiun0  45644  islptre  46071  salgenval  46771  salgenn0  46781  salgencl  46782  sssalgen  46785  salgenss  46786  salgenuni  46787  issalgend  46788  dfsalgen2  46791  salgencntex  46793  dfclnbgr3  48324  predgclnbgrel  48337  clnbgredg  48338  clnbgrgrimlem  48431  clnbgrgrim  48432  opndisj  49400  opnneilem  49403  sepfsepc  49425  iscnrm3rlem8  49444  iscnrm3llem2  49447  intubeu  49481  ipolubdm  49484  ipoglbdm  49487  setrec1lem1  50184  setrec1lem3  50186  setrec2fun  50189