MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseq2 Structured version   Visualization version   GIF version

Theorem sseq2 3586
Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
Assertion
Ref Expression
sseq2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))

Proof of Theorem sseq2
StepHypRef Expression
1 sstr2 3571 . . . 4 (𝐶𝐴 → (𝐴𝐵𝐶𝐵))
21com12 32 . . 3 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
3 sstr2 3571 . . . 4 (𝐶𝐵 → (𝐵𝐴𝐶𝐴))
43com12 32 . . 3 (𝐵𝐴 → (𝐶𝐵𝐶𝐴))
52, 4anim12i 587 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
6 eqss 3579 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
7 dfbi2 657 . 2 ((𝐶𝐴𝐶𝐵) ↔ ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
85, 6, 73imtr4i 279 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wss 3536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-in 3543  df-ss 3550
This theorem is referenced by:  sseq12  3587  sseq2i  3589  sseq2d  3592  syl5sseq  3612  nssne1  3620  psseq2  3653  sseq0  3923  un00  3959  disjpss  3976  pweq  4107  ssintab  4420  ssintub  4421  intmin  4423  treq  4677  sseliALT  4711  ssexg  4724  intabs  4744  ordunidif  5673  ordssun  5727  fununi  5861  feq3  5924  ssimaexg  6156  iunpw  6844  tfindsg  6926  limomss  6936  findsg  6959  funcnvuni  6986  frxp  7148  wrecseq123  7269  wfrlem1  7275  wfrlem4  7279  wfrlem15  7290  onfununi  7299  oawordeu  7496  oawordexr  7497  nnawordex  7578  ereq1  7610  xpider  7679  domeng  7829  sbthlem4  7932  sbthlem5  7933  domssex  7980  finsschain  8130  dffi2  8186  dffi3  8194  hartogslem1  8304  inf3lema  8378  cantnflem1  8443  tz9.1  8462  tz9.1c  8463  tctr  8473  tcmin  8474  tcrank  8604  scottex  8605  cardlim  8655  infxpenlem  8693  infxpenc2  8702  isinfcard  8772  alephinit  8775  alephval3  8790  dfac3  8801  cflem  8925  cfval  8926  cflecard  8932  cfsuc  8936  cff1  8937  cfflb  8938  cflim2  8942  isf32lem2  9033  fin1a2lem13  9091  ac7g  9153  ttukeylem5  9192  ttukeylem7  9194  pwcfsdom  9258  pwfseqlem5  9338  pwfseq  9339  gch2  9350  winalim  9370  wunex  9414  wuncss  9420  eltskg  9425  eltsk2g  9426  gruina  9493  grur1a  9494  axgroth6  9503  swrdnd2  13228  trcleq2lem  13521  dfrtrcl2  13593  fprodss  14460  mrcflem  16032  mrcval  16036  isacs2  16080  acsfiel  16081  ipoval  16920  fpwipodrs  16930  ipodrsima  16931  mreclatBAD  16953  slwispgp  17792  pgpssslw  17795  lsmss1b  17846  lsmss2b  17848  cntzcmnss  18012  gsumzres  18076  lspf  18738  lspval  18739  lbsextlem1  18922  lbsextlem3  18924  lbsextlem4  18925  aspval  19092  mplsubglem  19198  mpllsslem  19199  basis2  20505  eltg2  20512  clsval  20590  clscld  20600  clsval2  20603  ntrcls0  20629  isnei  20656  neiint  20657  neips  20666  opnneissb  20667  opnssneib  20668  neindisj2  20676  innei  20678  neiptoptop  20684  neiptopnei  20685  neitr  20733  restcls  20734  cnpimaex  20809  cnprest2  20843  regsep  20887  nrmsep3  20908  nrmsep  20910  regsep2  20929  tgcmp  20953  uncmp  20955  bwth  20962  1stcfb  20997  1stcrest  21005  2ndcctbss  21007  1stcelcls  21013  lly1stc  21048  ssref  21064  refref  21065  comppfsc  21084  xkoopn  21141  neitx  21159  txcnp  21172  txcmplem1  21193  kqnrmlem1  21295  kqnrmlem2  21296  nrmhmph  21346  fbssfi  21390  opnfbas  21395  fbasfip  21421  fbunfip  21422  fgss2  21427  fgcl  21431  supfil  21448  isufil2  21461  filssufilg  21464  ssufl  21471  ufileu  21472  elfm3  21503  fmfnfm  21511  ufldom  21515  fbflim2  21530  flfneii  21545  flftg  21549  txflf  21559  supnfcls  21573  fclscf  21578  fclsfnflim  21580  flimfnfcls  21581  alexsubALTlem2  21601  alexsubALTlem3  21602  alexsubALTlem4  21603  alexsubALT  21604  tsmsfbas  21680  tsmsres  21696  tsmsf1o  21697  tsmsxplem1  21705  tsmsxp  21707  ustssel  21758  ustincl  21760  ustdiag  21761  ustinvel  21762  ustexhalf  21763  ust0  21772  elutop  21786  ustuqtop4  21797  cfiluexsm  21843  cfiluweak  21848  blssps  21977  blss  21978  metss  22061  metrest  22077  metcnp3  22093  metnrmlem3  22400  lebnumlem3  22498  lebnum  22499  ellimc3  23363  lhop1lem  23494  dchrelbas  24675  avril1  26474  spanval  27379  spancl  27382  shsval2i  27433  omlsi  27450  ococin  27454  chsupsn  27459  pjoml  27482  shs00i  27496  chj00i  27533  chsscon3  27546  chlejb1  27558  chnle  27560  pjoml2  27657  pjoml3  27658  lecm  27663  stcltr1i  28320  mdbr  28340  dmdmd  28346  dmdi  28348  dmdbr3  28351  dmdbr4  28352  mdsl1i  28367  mdslmd1lem3  28373  mdslmd1lem4  28374  csmdsymi  28380  hatomic  28406  chrelat2  28416  atord  28434  atcvat4i  28443  fz1nntr  28751  reff  29037  cmpcref  29048  sigagenval  29333  dmsigagen  29337  sigagenss  29342  ldsysgenld  29353  ldgenpisyslem1  29356  ldgenpisyslem2  29357  dynkin  29360  carsgmon  29506  carsgclctunlem2  29511  bnj1286  30144  bnj1452  30177  kur14lem9  30253  mclsssvlem  30516  mclsind  30524  frrlem1  30827  frrlem4  30830  frrlem5e  30835  frrlem11  30839  imagesset  31033  altopthsn  31041  fnessref  31325  refssfne  31326  topjoin  31333  neifg  31339  bj-snglex  31954  relowlssretop  32187  relowlpssretop  32188  finxpreclem3  32206  poimirlem29  32408  poimir  32412  mblfinlem3  32418  totbndss  32546  heibor1lem  32578  unichnidl  32800  ispridl  32803  maxidlmax  32812  igenval  32830  igenidl  32832  igenmin  32833  igenval2  32835  lsatcmp  33108  lcvexchlem4  33142  lcvexchlem5  33143  pclvalN  33994  pclclN  33995  elpcliN  33997  docaclN  35231  dihglb2  35449  doch2val2  35471  dochocss  35473  dochexmidlem7  35573  lpolconN  35594  mapdval  35735  nacsfix  36093  mzpcompact2  36133  rgspnval  36557  rgspncl  36558  rgspnmin  36560  superficl  36691  superuncl  36692  cleq2lem  36733  clcnvlem  36749  dfrtrcl3  36844  clsk1indlem2  37160  neik0pk1imk0  37165  isotone1  37166  isotone2  37167  ntrclsiso  37185  gneispacess2  37264  ssrecnpr  37329  founiiun  38155  founiiun0  38172  islptre  38487  salgenval  39018  salgenn0  39026  salgencl  39027  sssalgen  39030  salgenss  39031  salgenuni  39032  issalgend  39033  dfsalgen2  39036  salgencntex  39038  iunopeqop  40128  upgredgpr  40373  dfnbgr3  40561  nbupgr  40565  nbumgrvtx  40567  nbgr2vtx1edg  40571  nbuhgr2vtx1edgb  40573  cusgrexi  40661  1wlkvtxiedg  40828  1wlkres  40878  upgr11wlkdlem2  41312  1pthon2v-av  41319  1pthon2ve  41320  cusconngr  41357
  Copyright terms: Public domain W3C validator