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

Theorem sseq2 3756
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 3739 . . . 4 (𝐶𝐴 → (𝐴𝐵𝐶𝐵))
21com12 32 . . 3 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
3 sstr2 3739 . . . 4 (𝐶𝐵 → (𝐵𝐴𝐶𝐴))
43com12 32 . . 3 (𝐵𝐴 → (𝐶𝐵𝐶𝐴))
52, 4anim12i 591 . 2 ((𝐴𝐵𝐵𝐴) → ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
6 eqss 3747 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
7 dfbi2 663 . 2 ((𝐶𝐴𝐶𝐵) ↔ ((𝐶𝐴𝐶𝐵) ∧ (𝐶𝐵𝐶𝐴)))
85, 6, 73imtr4i 281 1 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1620  wss 3703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-in 3710  df-ss 3717
This theorem is referenced by:  sseq12  3757  sseq2i  3759  sseq2d  3762  syl5sseq  3782  nssne1  3790  psseq2  3825  sseq0  4106  un00  4142  disjpss  4160  pweq  4293  ssintab  4634  ssintub  4635  intmin  4637  treq  4898  sseliALT  4931  ssexg  4944  intabs  4962  iunopeqop  5119  ordunidif  5922  ordssun  5976  fununi  6113  feq3  6177  ssimaexg  6414  iunpw  7131  tfindsg  7213  limomss  7223  findsg  7246  funcnvuni  7272  frxp  7443  wrecseq123  7565  wfrlem1  7571  wfrlem4  7575  wfrlem15  7586  onfununi  7595  oawordeu  7792  oawordexr  7793  nnawordex  7874  ereq1  7906  xpider  7973  domeng  8123  sbthlem4  8226  sbthlem5  8227  domssex  8274  finsschain  8426  dffi2  8482  dffi3  8490  hartogslem1  8600  inf3lema  8682  cantnflem1  8747  tz9.1  8766  tz9.1c  8767  tctr  8777  tcmin  8778  tcrank  8908  scottex  8909  cardlim  8959  infxpenlem  8997  infxpenc2  9006  isinfcard  9076  alephinit  9079  alephval3  9094  dfac3  9105  cflem  9231  cfval  9232  cflecard  9238  cfsuc  9242  cff1  9243  cfflb  9244  cflim2  9248  isf32lem2  9339  fin1a2lem13  9397  ac7g  9459  ttukeylem5  9498  ttukeylem7  9500  pwcfsdom  9568  pwfseqlem5  9648  pwfseq  9649  gch2  9660  winalim  9680  wunex  9724  wuncss  9730  eltskg  9735  eltsk2g  9736  gruina  9803  grur1a  9804  axgroth6  9813  swrdnd2  13604  trcleq2lem  13902  dfrtrcl2  13972  fprodss  14848  mrcflem  16439  mrcval  16443  isacs2  16486  acsfiel  16487  ipoval  17326  fpwipodrs  17336  ipodrsima  17337  mreclatBAD  17359  slwispgp  18197  pgpssslw  18200  lsmss1b  18251  lsmss2b  18253  cntzcmnss  18417  gsumzres  18481  lspf  19147  lspval  19148  lbsextlem1  19331  lbsextlem3  19333  lbsextlem4  19334  aspval  19501  mplsubglem  19607  mpllsslem  19608  basis2  20928  eltg2  20935  clsval  21014  clscld  21024  clsval2  21027  ntrcls0  21053  isnei  21080  neiint  21081  neips  21090  opnneissb  21091  opnssneib  21092  neindisj2  21100  innei  21102  neiptoptop  21108  neiptopnei  21109  neitr  21157  restcls  21158  cnpimaex  21233  cnprest2  21267  regsep  21311  nrmsep3  21332  nrmsep  21334  regsep2  21353  tgcmp  21377  uncmp  21379  bwth  21386  1stcfb  21421  1stcrest  21429  2ndcctbss  21431  1stcelcls  21437  lly1stc  21472  ssref  21488  refref  21489  comppfsc  21508  xkoopn  21565  neitx  21583  txcnp  21596  txcmplem1  21617  kqnrmlem1  21719  kqnrmlem2  21720  nrmhmph  21770  fbssfi  21813  opnfbas  21818  fbasfip  21844  fbunfip  21845  fgss2  21850  fgcl  21854  supfil  21871  isufil2  21884  filssufilg  21887  ssufl  21894  ufileu  21895  elfm3  21926  fmfnfm  21934  ufldom  21938  fbflim2  21953  flfneii  21968  flftg  21972  txflf  21982  supnfcls  21996  fclscf  22001  fclsfnflim  22003  flimfnfcls  22004  alexsubALTlem2  22024  alexsubALTlem3  22025  alexsubALTlem4  22026  alexsubALT  22027  tsmsfbas  22103  tsmsres  22119  tsmsf1o  22120  tsmsxplem1  22128  tsmsxp  22130  ustssel  22181  ustincl  22183  ustdiag  22184  ustinvel  22185  ustexhalf  22186  ust0  22195  elutop  22209  ustuqtop4  22220  cfiluexsm  22266  cfiluweak  22271  blssps  22401  blss  22402  metss  22485  metrest  22501  metcnp3  22517  metnrmlem3  22836  lebnumlem3  22934  lebnum  22935  ellimc3  23813  lhop1lem  23946  dchrelbas  25131  upgredgpr  26207  dfnbgr3  26401  nbupgr  26410  nbumgrvtx  26412  nbgr2vtx1edg  26416  nbuhgr2vtx1edgb  26418  cusgrexilem2  26519  wlkvtxiedg  26701  wlkres  26748  upgr1wlkdlem2  27269  1pthon2v  27276  1pthon2ve  27277  cusconngr  27314  avril1  27601  spanval  28472  spancl  28475  shsval2i  28526  omlsi  28543  ococin  28547  chsupsn  28552  pjoml  28575  shs00i  28589  chj00i  28626  chsscon3  28639  chlejb1  28651  chnle  28653  pjoml2  28750  pjoml3  28751  lecm  28756  stcltr1i  29413  mdbr  29433  dmdmd  29439  dmdi  29441  dmdbr3  29444  dmdbr4  29445  mdsl1i  29460  mdslmd1lem3  29466  mdslmd1lem4  29467  csmdsymi  29473  hatomic  29499  chrelat2  29509  atord  29527  atcvat4i  29536  fz1nntr  29841  reff  30186  cmpcref  30197  sigagenval  30483  dmsigagen  30487  sigagenss  30492  ldsysgenld  30503  ldgenpisyslem1  30506  ldgenpisyslem2  30507  dynkin  30510  carsgmon  30656  carsgclctunlem2  30661  bnj1286  31365  bnj1452  31398  kur14lem9  31474  mclsssvlem  31737  mclsind  31745  frrlem1  32057  scutun12  32194  imagesset  32337  altopthsn  32345  fnessref  32629  refssfne  32630  topjoin  32637  neifg  32643  bj-snglex  33238  relowlssretop  33493  relowlpssretop  33494  finxpreclem3  33512  poimirlem29  33720  poimir  33724  mblfinlem3  33730  totbndss  33858  heibor1lem  33890  unichnidl  34112  ispridl  34115  maxidlmax  34124  igenval  34142  igenidl  34144  igenmin  34145  igenval2  34147  brssr  34543  lsatcmp  34762  lcvexchlem4  34796  lcvexchlem5  34797  pclvalN  35648  pclclN  35649  elpcliN  35651  docaclN  36884  dihglb2  37102  doch2val2  37124  dochocss  37126  dochexmidlem7  37226  lpolconN  37247  mapdval  37388  nacsfix  37746  mzpcompact2  37786  rgspnval  38209  rgspncl  38210  rgspnmin  38212  superficl  38343  superuncl  38344  cleq2lem  38385  clcnvlem  38401  dfrtrcl3  38496  clsk1indlem2  38811  neik0pk1imk0  38816  isotone1  38817  isotone2  38818  ntrclsiso  38836  gneispacess2  38915  ssrecnpr  38978  founiiun  39828  founiiun0  39845  islptre  40323  salgenval  41013  salgenn0  41021  salgencl  41022  sssalgen  41025  salgenss  41026  salgenuni  41027  issalgend  41028  dfsalgen2  41031  salgencntex  41033  setrec1lem1  42913  setrec1lem3  42915  setrec2fun  42918
  Copyright terms: Public domain W3C validator