Theorem sseq2 3957

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  sseq12  3958  sseq2i  3960  sseq2d  3963  nssne1  3993  psseq2  4039  sseq0b  4353  un00  4357  disjpss  4414  pweqALT  4572  ssintab  4925  ssintub  4926  intmin  4928  treq  5219  al0ssb  5262  sseliALT  5263  ssexgOLD  5285  intabs  5310  iunopeqop  5494  iunopeqopOLD  5495  onelssex  6405  ordunidif  6406  ordssun  6460  fununi  6607  feq3  6681  ssimaexg  6963  fnssintima  7364  iunpw  7774  tfindsg  7861  limomss  7871  findsg  7898  funcnvuni  7933  frxp  8127  frrlem1  8288  frrlem13  8300  onfununi  8333  oawordeu  8547  oawordexr  8548  nnawordex  8630  eldifsucnn  8657  coflton  8664  cofon1  8665  cofon2  8666  cofonr  8667  naddcllem  8669  naddunif  8687  ereq1  8709  xpider  8793  domeng  8973  sbthlem4  9093  sbthlem5  9094  domssex  9141  ssfi  9172  finsschain  9332  dffi2  9399  dffi3  9407  hartogslem1  9520  inf3lema  9609  cantnflem1  9674  dfttrcl2  9709  tz9.1  9714  tz9.1c  9715  tctr  9723  tcmin  9724  tcrank  9882  scottex  9914  scottexOLD  9915  setrec1lem1  9947  setrec1lem3  9950  setrec2fun  9954  cardlim  10034  infxpenlem  10073  infxpenc2  10082  isinfcard  10152  alephinit  10155  alephval3  10170  dfac3  10181  cflem  10304  cfval  10305  cflecard  10311  cfsuc  10316  cff1  10317  cfflb  10318  cflim2  10322  isf32lem2  10413  fin1a2lem13  10471  ac7g  10533  ttukeylem5  10572  ttukeylem7  10574  pwcfsdom  10649  pwfseqlem5  10729  pwfseq  10730  gch2  10741  winalim  10761  wunex  10805  wuncss  10811  eltskg  10816  eltsk2g  10817  gruina  10884  grur1a  10885  axgroth6  10894  swrdnd2  14785  trcleq2lem  15124  dfrtrcl2  15195  fprodss  16095  mrcflem  17760  mrcval  17764  isacs2  17807  acsfiel  17808  ipoval  18684  fpwipodrs  18694  ipodrsima  18695  mreclatBAD  18717  slwispgp  19805  pgpssslw  19808  lsmss1b  19860  lsmss2b  19862  cntzcmnss  20035  gsumzres  20103  rgspnval  20844  rgspncl  20845  rgspnmin  20847  lspf  21229  lspval  21230  lbsextlem1  21416  lbsextlem3  21418  lbsextlem4  21419  unichnlidl  21496  rspprop  21504  isprmidl  21599  ssdifidllem  21620  ssdifidl  21621  ssdifidlprm  21622  aspval  22160  mplsubglem  22286  mpllsslem  22287  basis2  23249  eltg2  23256  clsval  23335  clscld  23345  clsval2  23348  ntrcls0  23374  isnei  23401  neiint  23402  neips  23411  opnneissb  23412  opnssneib  23413  neindisj2  23421  innei  23423  neiptoptop  23429  neiptopnei  23430  neitr  23478  restcls  23479  cnpimaex  23554  cnprest2  23588  regsep  23632  nrmsep3  23653  nrmsep  23655  regsep2  23674  tgcmp  23699  uncmp  23701  bwth  23708  1stcfb  23743  1stcrest  23751  2ndcctbss  23754  1stcelcls  23760  lly1stc  23795  ssref  23811  refref  23812  comppfsc  23831  xkoopn  23888  neitx  23906  txcnp  23919  txcmplem1  23940  kqnrmlem1  24042  kqnrmlem2  24043  nrmhmph  24093  fbssfi  24136  opnfbas  24141  fbasfip  24167  fbunfip  24168  fgss2  24173  fgcl  24177  supfil  24194  isufil2  24207  filssufilg  24210  ssufl  24217  ufileu  24218  elfm3  24249  fmfnfm  24257  ufldom  24261  fbflim2  24276  flfneii  24291  flftg  24295  txflf  24305  supnfcls  24319  fclscf  24324  fclsfnflim  24326  flimfnfcls  24327  alexsubALTlem2  24347  alexsubALTlem3  24348  alexsubALTlem4  24349  alexsubALT  24350  tsmsfbas  24427  tsmsres  24443  tsmsf1o  24444  tsmsxplem1  24452  tsmsxp  24454  ustssel  24505  ustincl  24507  ustdiag  24508  ustinvel  24509  ustexhalf  24510  ust0  24519  elutop  24532  ustuqtop4  24543  cfiluexsm  24588  cfiluweak  24593  blssps  24723  blss  24724  metss  24807  metrest  24823  metcnp3  24839  metnrmlem3  25161  lebnumlem3  25264  lebnum  25265  ellimc3  26179  lhop1lem  26313  dchrelbas  27545  eqcuts2  28154  cutsun12  28158  madebdayim  28256  madebday  28268  oniso  28639  bdayn0p1  28737  prlngd  29399  dfprlng2  29407  upgredgpr  29702  dfnbgr3  29901  nbupgr  29907  nbumgrvtx  29909  nbgr2vtx1edg  29913  nbuhgr2vtx1edgb  29915  cusgrexilem2  30005  wlkvtxiedg  30187  wlkres  30231  upgr1wlkdlem2  30719  1pthon2v  30736  1pthon2ve  30737  cusconngr  30774  isfrgr  30843  avril1  31046  spanval  31917  spancl  31920  shsval2i  31971  omlsi  31988  ococin  31992  chsupsn  31997  pjoml  32020  shs00i  32034  chj00i  32071  chsscon3  32084  chlejb1  32096  chnle  32098  pjoml2  32195  pjoml3  32196  lecm  32201  stcltr1i  32858  mdbr  32878  dmdmd  32884  dmdi  32886  dmdbr3  32889  dmdbr4  32890  mdsl1i  32905  mdslmd1lem3  32911  mdslmd1lem4  32912  csmdsymi  32918  hatomic  32944  chrelat2  32954  atord  32972  atcvat4i  32981  fz1nntr  33376  elrgspnlem4  33788  fldgenval  33856  fldgensdrg  33858  fldgenssv  33859  fldgenssp  33862  nsgmgc  33945  nsgqusf1olem2  33947  mxidlmax  33972  ssmxidllem  33980  ssmxidl  33981  dflringlem  34008  1arithufdlem4  34061  reff  34453  cmpcref  34464  zarcls1  34483  zarclsiin  34485  zarclssn  34487  zart0  34493  zarmxt1  34494  zarcmp  34496  rhmpreimacnlem  34498  sigagenval  34755  dmsigagen  34759  sigagenss  34764  ldsysgenld  34775  ldgenpisyslem1  34778  ldgenpisyslem2  34779  dynkin  34782  carsgmon  34929  carsgclctunlem2  34934  bnj1286  35632  bnj1452  35665  fineqvac  35757  tz9.1regs  35775  onvf1odlem4  35858  vonf1wev  35860  vonf1owevOLD  35862  kur14lem9  35948  mclsssvlem  36296  mclsind  36304  imagesset  36687  altopthsn  36696  fnessref  37115  refssfne  37116  topjoin  37123  neifg  37129  tz9.1tco  37241  ttc00  37266  dfttc3gw  37281  bj-snglex  37856  bj-imdirvallem  38069  relowlssretop  38254  relowlpssretop  38255  exrecfnlem  38270  finxpreclem3  38284  pibt2  38308  poimirlem29  38535  poimir  38539  mblfinlem3  38545  totbndss  38679  heibor1lem  38711  unichnidl  38933  ispridl  38936  maxidlmax  38945  igenval  38963  igenidl  38965  igenmin  38966  igenval2  38968  dfsuccl4  39374  brssr  39481  suceldisj  39718  lsatcmp  40028  lcvexchlem4  40062  lcvexchlem5  40063  pclvalN  40915  pclclN  40916  elpcliN  40918  docaclN  42149  dihglb2  42367  doch2val2  42389  dochocss  42391  dochexmidlem7  42491  lpolconN  42512  mapdval  42653  nacsfix  43676  mzpcompact2  43716  superficl  44526  superuncl  44527  cleq2lem  44567  clcnvlem  44582  dfrtrcl3  44692  clsk1indlem2  45001  neik0pk1imk0  45006  isotone1  45007  isotone2  45008  ntrclsiso  45026  gneispacess2  45105  mnuunid  45220  mnurndlem2  45225  ssrecnpr  45251  founiiun  46137  founiiun0  46148  islptre  46575  salgenval  47275  salgenn0  47285  salgencl  47286  sssalgen  47289  salgenss  47290  salgenuni  47291  issalgend  47292  dfsalgen2  47295  salgencntex  47297  dfclnbgr3  48868  predgclnbgrel  48881  clnbgredg  48882  clnbgrgrimlem  48975  clnbgrgrim  48976  opndisj  49955  opnneilem  49958  sepfsepc  49980  iscnrm3rlem8  49999  iscnrm3llem2  50002  intubeu  50036  ipolubdm  50039  ipoglbdm  50042