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

Theorem sseq2 3612
 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 3595 . . . 4 (𝐶𝐴 → (𝐴𝐵𝐶𝐵))
21com12 32 . . 3 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
3 sstr2 3595 . . . 4 (𝐶𝐵 → (𝐵𝐴𝐶𝐴))
43com12 32 . . 3 (𝐵𝐴 → (𝐶𝐵𝐶𝐴))
52, 4anim12i 589 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
6 eqss 3603 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
7 dfbi2 659 . 2 ((𝐶𝐴𝐶𝐵) ↔ ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
85, 6, 73imtr4i 281 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ⊆ wss 3560 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574 This theorem is referenced by:  sseq12  3613  sseq2i  3615  sseq2d  3618  syl5sseq  3638  nssne1  3646  psseq2  3679  sseq0  3953  un00  3989  disjpss  4006  pweq  4139  ssintab  4466  ssintub  4467  intmin  4469  treq  4728  sseliALT  4761  ssexg  4774  intabs  4795  iunopeqop  4951  ordunidif  5742  ordssun  5796  fununi  5932  feq3  5995  ssimaexg  6231  iunpw  6940  tfindsg  7022  limomss  7032  findsg  7055  funcnvuni  7081  frxp  7247  wrecseq123  7368  wfrlem1  7374  wfrlem4  7378  wfrlem15  7389  onfununi  7398  oawordeu  7595  oawordexr  7596  nnawordex  7677  ereq1  7709  xpider  7778  domeng  7929  sbthlem4  8033  sbthlem5  8034  domssex  8081  finsschain  8233  dffi2  8289  dffi3  8297  hartogslem1  8407  inf3lema  8481  cantnflem1  8546  tz9.1  8565  tz9.1c  8566  tctr  8576  tcmin  8577  tcrank  8707  scottex  8708  cardlim  8758  infxpenlem  8796  infxpenc2  8805  isinfcard  8875  alephinit  8878  alephval3  8893  dfac3  8904  cflem  9028  cfval  9029  cflecard  9035  cfsuc  9039  cff1  9040  cfflb  9041  cflim2  9045  isf32lem2  9136  fin1a2lem13  9194  ac7g  9256  ttukeylem5  9295  ttukeylem7  9297  pwcfsdom  9365  pwfseqlem5  9445  pwfseq  9446  gch2  9457  winalim  9477  wunex  9521  wuncss  9527  eltskg  9532  eltsk2g  9533  gruina  9600  grur1a  9601  axgroth6  9610  swrdnd2  13387  trcleq2lem  13680  dfrtrcl2  13752  fprodss  14622  mrcflem  16206  mrcval  16210  isacs2  16254  acsfiel  16255  ipoval  17094  fpwipodrs  17104  ipodrsima  17105  mreclatBAD  17127  slwispgp  17966  pgpssslw  17969  lsmss1b  18020  lsmss2b  18022  cntzcmnss  18186  gsumzres  18250  lspf  18914  lspval  18915  lbsextlem1  19098  lbsextlem3  19100  lbsextlem4  19101  aspval  19268  mplsubglem  19374  mpllsslem  19375  basis2  20695  eltg2  20702  clsval  20781  clscld  20791  clsval2  20794  ntrcls0  20820  isnei  20847  neiint  20848  neips  20857  opnneissb  20858  opnssneib  20859  neindisj2  20867  innei  20869  neiptoptop  20875  neiptopnei  20876  neitr  20924  restcls  20925  cnpimaex  21000  cnprest2  21034  regsep  21078  nrmsep3  21099  nrmsep  21101  regsep2  21120  tgcmp  21144  uncmp  21146  bwth  21153  1stcfb  21188  1stcrest  21196  2ndcctbss  21198  1stcelcls  21204  lly1stc  21239  ssref  21255  refref  21256  comppfsc  21275  xkoopn  21332  neitx  21350  txcnp  21363  txcmplem1  21384  kqnrmlem1  21486  kqnrmlem2  21487  nrmhmph  21537  fbssfi  21581  opnfbas  21586  fbasfip  21612  fbunfip  21613  fgss2  21618  fgcl  21622  supfil  21639  isufil2  21652  filssufilg  21655  ssufl  21662  ufileu  21663  elfm3  21694  fmfnfm  21702  ufldom  21706  fbflim2  21721  flfneii  21736  flftg  21740  txflf  21750  supnfcls  21764  fclscf  21769  fclsfnflim  21771  flimfnfcls  21772  alexsubALTlem2  21792  alexsubALTlem3  21793  alexsubALTlem4  21794  alexsubALT  21795  tsmsfbas  21871  tsmsres  21887  tsmsf1o  21888  tsmsxplem1  21896  tsmsxp  21898  ustssel  21949  ustincl  21951  ustdiag  21952  ustinvel  21953  ustexhalf  21954  ust0  21963  elutop  21977  ustuqtop4  21988  cfiluexsm  22034  cfiluweak  22039  blssps  22169  blss  22170  metss  22253  metrest  22269  metcnp3  22285  metnrmlem3  22604  lebnumlem3  22702  lebnum  22703  ellimc3  23583  lhop1lem  23714  dchrelbas  24895  upgredgpr  25966  dfnbgr3  26157  nbupgr  26161  nbumgrvtx  26163  nbgr2vtx1edg  26167  nbuhgr2vtx1edgb  26169  cusgrexilem2  26259  wlkvtxiedg  26424  wlkres  26470  upgr1wlkdlem2  26906  1pthon2v  26913  1pthon2ve  26914  cusconngr  26951  avril1  27207  spanval  28080  spancl  28083  shsval2i  28134  omlsi  28151  ococin  28155  chsupsn  28160  pjoml  28183  shs00i  28197  chj00i  28234  chsscon3  28247  chlejb1  28259  chnle  28261  pjoml2  28358  pjoml3  28359  lecm  28364  stcltr1i  29021  mdbr  29041  dmdmd  29047  dmdi  29049  dmdbr3  29052  dmdbr4  29053  mdsl1i  29068  mdslmd1lem3  29074  mdslmd1lem4  29075  csmdsymi  29081  hatomic  29107  chrelat2  29117  atord  29135  atcvat4i  29144  fz1nntr  29444  reff  29730  cmpcref  29741  sigagenval  30026  dmsigagen  30030  sigagenss  30035  ldsysgenld  30046  ldgenpisyslem1  30049  ldgenpisyslem2  30050  dynkin  30053  carsgmon  30199  carsgclctunlem2  30204  bnj1286  30848  bnj1452  30881  kur14lem9  30957  mclsssvlem  31220  mclsind  31228  frrlem1  31534  frrlem4  31537  frrlem5e  31542  frrlem11  31546  imagesset  31755  altopthsn  31763  fnessref  32047  refssfne  32048  topjoin  32055  neifg  32061  bj-snglex  32661  relowlssretop  32882  relowlpssretop  32883  finxpreclem3  32901  poimirlem29  33109  poimir  33113  mblfinlem3  33119  totbndss  33247  heibor1lem  33279  unichnidl  33501  ispridl  33504  maxidlmax  33513  igenval  33531  igenidl  33533  igenmin  33534  igenval2  33536  lsatcmp  33809  lcvexchlem4  33843  lcvexchlem5  33844  pclvalN  34695  pclclN  34696  elpcliN  34698  docaclN  35932  dihglb2  36150  doch2val2  36172  dochocss  36174  dochexmidlem7  36274  lpolconN  36295  mapdval  36436  nacsfix  36794  mzpcompact2  36834  rgspnval  37258  rgspncl  37259  rgspnmin  37261  superficl  37392  superuncl  37393  cleq2lem  37434  clcnvlem  37450  dfrtrcl3  37545  clsk1indlem2  37861  neik0pk1imk0  37866  isotone1  37867  isotone2  37868  ntrclsiso  37886  gneispacess2  37965  ssrecnpr  38028  founiiun  38869  founiiun0  38886  islptre  39287  salgenval  39878  salgenn0  39886  salgencl  39887  sssalgen  39890  salgenss  39891  salgenuni  39892  issalgend  39893  dfsalgen2  39896  salgencntex  39898  setrec1lem1  41757  setrec1lem3  41759  setrec2fun  41762
 Copyright terms: Public domain W3C validator