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

Theorem sseq2 3990
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 3971 . . . 4 (𝐶𝐴 → (𝐴𝐵𝐶𝐵))
21com12 32 . . 3 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
3 sstr2 3971 . . . 4 (𝐶𝐵 → (𝐵𝐴𝐶𝐴))
43com12 32 . . 3 (𝐵𝐴 → (𝐶𝐵𝐶𝐴))
52, 4anim12i 612 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
6 eqss 3979 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
7 dfbi2 475 . 2 ((𝐶𝐴𝐶𝐵) ↔ ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
85, 6, 73imtr4i 293 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  sseq12  3991  sseq2i  3993  sseq2d  3996  sseqtrid  4016  nssne1  4024  psseq2  4062  sseq0  4350  un00  4390  disjpss  4406  pweq  4538  ssintab  4884  ssintub  4885  intmin  4887  treq  5169  al0ssb  5203  sseliALT  5204  ssexg  5218  intabs  5236  iunopeqop  5402  ordunidif  6232  ordssun  6283  fununi  6422  feq3  6490  ssimaexg  6742  iunpw  7482  tfindsg  7564  limomss  7574  findsg  7598  funcnvuni  7625  frxp  7809  wrecseq123  7937  wfrlem1  7943  wfrlem4  7947  wfrlem15  7958  onfununi  7967  oawordeu  8170  oawordexr  8171  nnawordex  8252  ereq1  8285  xpider  8357  domeng  8511  sbthlem4  8618  sbthlem5  8619  domssex  8666  finsschain  8819  dffi2  8875  dffi3  8883  hartogslem1  8994  inf3lema  9075  cantnflem1  9140  tz9.1  9159  tz9.1c  9160  tctr  9170  tcmin  9171  tcrank  9301  scottex  9302  cardlim  9389  infxpenlem  9427  infxpenc2  9436  isinfcard  9506  alephinit  9509  alephval3  9524  dfac3  9535  cflem  9656  cfval  9657  cflecard  9663  cfsuc  9667  cff1  9668  cfflb  9669  cflim2  9673  isf32lem2  9764  fin1a2lem13  9822  ac7g  9884  ttukeylem5  9923  ttukeylem7  9925  pwcfsdom  9993  pwfseqlem5  10073  pwfseq  10074  gch2  10085  winalim  10105  wunex  10149  wuncss  10155  eltskg  10160  eltsk2g  10161  gruina  10228  grur1a  10229  axgroth6  10238  swrdnd2  14005  trcleq2lem  14339  dfrtrcl2  14409  fprodss  15290  mrcflem  16865  mrcval  16869  isacs2  16912  acsfiel  16913  ipoval  17752  fpwipodrs  17762  ipodrsima  17763  mreclatBAD  17785  slwispgp  18665  pgpssslw  18668  lsmss1b  18721  lsmss2b  18723  cntzcmnss  18890  gsumzres  18958  lspf  19675  lspval  19676  lbsextlem1  19859  lbsextlem3  19861  lbsextlem4  19862  aspval  20030  mplsubglem  20142  mpllsslem  20143  basis2  21487  eltg2  21494  clsval  21573  clscld  21583  clsval2  21586  ntrcls0  21612  isnei  21639  neiint  21640  neips  21649  opnneissb  21650  opnssneib  21651  neindisj2  21659  innei  21661  neiptoptop  21667  neiptopnei  21668  neitr  21716  restcls  21717  cnpimaex  21792  cnprest2  21826  regsep  21870  nrmsep3  21891  nrmsep  21893  regsep2  21912  tgcmp  21937  uncmp  21939  bwth  21946  1stcfb  21981  1stcrest  21989  2ndcctbss  21991  1stcelcls  21997  lly1stc  22032  ssref  22048  refref  22049  comppfsc  22068  xkoopn  22125  neitx  22143  txcnp  22156  txcmplem1  22177  kqnrmlem1  22279  kqnrmlem2  22280  nrmhmph  22330  fbssfi  22373  opnfbas  22378  fbasfip  22404  fbunfip  22405  fgss2  22410  fgcl  22414  supfil  22431  isufil2  22444  filssufilg  22447  ssufl  22454  ufileu  22455  elfm3  22486  fmfnfm  22494  ufldom  22498  fbflim2  22513  flfneii  22528  flftg  22532  txflf  22542  supnfcls  22556  fclscf  22561  fclsfnflim  22563  flimfnfcls  22564  alexsubALTlem2  22584  alexsubALTlem3  22585  alexsubALTlem4  22586  alexsubALT  22587  tsmsfbas  22663  tsmsres  22679  tsmsf1o  22680  tsmsxplem1  22688  tsmsxp  22690  ustssel  22741  ustincl  22743  ustdiag  22744  ustinvel  22745  ustexhalf  22746  ust0  22755  elutop  22769  ustuqtop4  22780  cfiluexsm  22826  cfiluweak  22831  blssps  22961  blss  22962  metss  23045  metrest  23061  metcnp3  23077  metnrmlem3  23396  lebnumlem3  23494  lebnum  23495  ellimc3  24404  lhop1lem  24537  dchrelbas  25739  upgredgpr  26854  dfnbgr3  27047  nbupgr  27053  nbumgrvtx  27055  nbgr2vtx1edg  27059  nbuhgr2vtx1edgb  27061  cusgrexilem2  27151  wlkvtxiedg  27333  wlkres  27379  upgr1wlkdlem2  27852  1pthon2v  27859  1pthon2ve  27860  cusconngr  27897  isfrgr  27966  avril1  28169  spanval  29037  spancl  29040  shsval2i  29091  omlsi  29108  ococin  29112  chsupsn  29117  pjoml  29140  shs00i  29154  chj00i  29191  chsscon3  29204  chlejb1  29216  chnle  29218  pjoml2  29315  pjoml3  29316  lecm  29321  stcltr1i  29978  mdbr  29998  dmdmd  30004  dmdi  30006  dmdbr3  30009  dmdbr4  30010  mdsl1i  30025  mdslmd1lem3  30031  mdslmd1lem4  30032  csmdsymi  30038  hatomic  30064  chrelat2  30074  atord  30092  atcvat4i  30101  fz1nntr  30453  isprmidl  30874  reff  31002  cmpcref  31013  sigagenval  31298  dmsigagen  31302  sigagenss  31307  ldsysgenld  31318  ldgenpisyslem1  31321  ldgenpisyslem2  31322  dynkin  31325  carsgmon  31471  carsgclctunlem2  31476  bnj1286  32188  bnj1452  32221  kur14lem9  32358  mclsssvlem  32706  mclsind  32714  frrlem1  33020  frrlem13  33032  scutun12  33168  imagesset  33311  altopthsn  33319  fnessref  33602  refssfne  33603  topjoin  33610  neifg  33616  bj-snglex  34182  bj-imdirval  34364  relowlssretop  34526  relowlpssretop  34527  exrecfnlem  34542  finxpreclem3  34556  pibt2  34580  poimirlem29  34802  poimir  34806  mblfinlem3  34812  totbndss  34936  heibor1lem  34968  unichnidl  35190  ispridl  35193  maxidlmax  35202  igenval  35220  igenidl  35222  igenmin  35223  igenval2  35225  brssr  35621  lsatcmp  36019  lcvexchlem4  36053  lcvexchlem5  36054  pclvalN  36906  pclclN  36907  elpcliN  36909  docaclN  38140  dihglb2  38358  doch2val2  38380  dochocss  38382  dochexmidlem7  38482  lpolconN  38503  mapdval  38644  nacsfix  39187  mzpcompact2  39227  rgspnval  39646  rgspncl  39647  rgspnmin  39649  superficl  39804  superuncl  39805  cleq2lem  39846  clcnvlem  39861  dfrtrcl3  39956  clsk1indlem2  40270  neik0pk1imk0  40275  isotone1  40276  isotone2  40277  ntrclsiso  40295  gneispacess2  40374  mnuunid  40490  mnurndlem2  40495  ssrecnpr  40517  founiiun  41311  founiiun0  41327  islptre  41776  salgenval  42483  salgenn0  42491  salgencl  42492  sssalgen  42495  salgenss  42496  salgenuni  42497  issalgend  42498  dfsalgen2  42501  salgencntex  42503  isomgreqve  43867  setrec1lem1  44718  setrec1lem3  44720  setrec2fun  44723
  Copyright terms: Public domain W3C validator