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

Theorem eqssd 3584
Description: Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.)
Hypotheses
Ref Expression
eqssd.1 (𝜑𝐴𝐵)
eqssd.2 (𝜑𝐵𝐴)
Assertion
Ref Expression
eqssd (𝜑𝐴 = 𝐵)

Proof of Theorem eqssd
StepHypRef Expression
1 eqssd.1 . 2 (𝜑𝐴𝐵)
2 eqssd.2 . 2 (𝜑𝐵𝐴)
3 eqss 3582 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3sylanbrc 694 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wss 3539
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 2033  ax-13 2233  ax-ext 2589
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 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  eqrd  3585  uneqdifeq  4008  uneqdifeqOLD  4009  unissel  4398  intmin  4426  unissint  4430  int0el  4437  dmcosseq  5294  sofld  5485  relfld  5563  preddowncl  5609  wfi  5615  tz7.7  5651  fimacnv  6239  knatar  6484  sorpssuni  6821  sorpssint  6822  onint  6864  fo2ndf  7148  suppimacnv  7170  tposeq  7218  wfrlem10  7288  onfununi  7302  tfrlem15  7352  oaass  7505  odi  7523  omass  7524  oelim2  7539  oeeui  7546  nnawordex  7581  oaabslem  7587  oaabs2  7589  omabslem  7590  omabs  7591  uniinqs  7691  sucdom2  8018  fineqv  8037  dffi2  8189  fiuni  8194  dffi3  8197  ordtypelem9  8291  ordtypelem10  8292  oismo  8305  hartogslem1  8307  ixpiunwdom  8356  cantnfp1lem3  8437  oemapvali  8441  cantnf  8450  r1val1  8509  rankval3b  8549  rankunb  8573  rankuni2b  8576  rankr1id  8585  rankc2  8594  rankxplim  8602  tcrank  8607  carden2b  8653  harval2  8683  en2other2  8692  infpwfien  8745  coflim  8943  cfcof  8956  cfidm  8957  isf32lem2  9036  fin1a2lem11  9092  fin1a2lem13  9094  ttukeylem7  9197  fpwwe2  9321  winafp  9375  wuncidm  9424  wuncval2  9425  tskuni  9461  grur1  9498  distrpr  9706  prlem934  9711  ltexpri  9721  reclem4pr  9728  fzopth  12206  fzosplit  12327  fzouzsplit  12329  ccatrn  13173  cotrtrclfv  13549  dmtrclfv  13555  dfrtrcl2  13598  phimullem  15270  prmreclem5  15410  structcnvcnv  15654  imasaddfnlem  15959  imasvscafn  15968  mrcuni  16052  mressmrcd  16058  submrc  16059  ssceq  16257  rescabs  16264  setcepi  16509  clatl  16887  ipopos  16931  psdmrn  16978  psssdm2  16986  dirdm  17005  gsumress  17047  gsumvallem2  17143  gsumwspan  17154  cycsubg  17393  conjnmz  17465  pmtrprfv  17644  symggen  17661  odf1o2  17759  gex1  17777  sylow2alem1  17803  sylow3lem3  17815  lsmidm  17848  lsmss1  17850  lsmss2  17852  lsmmod  17859  lsmdisj  17865  lsmdisj2  17866  cntzcmn  18016  prmcyg  18066  dmdprdd  18169  dprdspan  18197  dprdres  18198  dprdz  18200  subgdmdprd  18204  subgdprd  18205  dprddisj2  18209  dprd2dlem1  18211  dprd2da  18212  dmdprdsplit2lem  18215  dprdsplit  18218  ablfacrp  18236  pgpfac1lem3  18247  kerf1hrm  18514  isdrng2  18528  issubdrg  18576  lspun  18756  lspsn  18771  lspsnneg  18775  lsp0  18778  lsslsp  18784  lmhmlsp  18818  lspextmo  18825  lsmsp  18855  lspprabs  18864  lspsnvs  18883  lspdisj  18894  lsmcv  18910  lspsnat  18914  lsppratlem6  18921  lspprat  18922  lbsextlem4  18930  lidl1el  18987  drngnidl  18998  lidldvgen  19024  fidomndrng  19076  mplbas2  19239  cnsubrg  19573  mulgrhm2  19613  znrrg  19680  ocvin  19784  ocvlsp  19786  mrccss  19804  pjfo  19825  obs2ss  19839  frlmsslsp  19901  topsn  20497  eltg4i  20522  unitg  20529  tgtop  20535  tgidm  20542  en2top  20547  basgen  20550  2basgen  20552  fctop  20565  cctop  20567  ppttop  20568  epttop  20570  ntrin  20622  isopn3  20627  opnnei  20681  neiuni  20683  maxlp  20708  clslp  20709  tgrest  20720  resttopon  20722  rest0  20730  restfpw  20740  restcls  20742  restntr  20743  ordtbas2  20752  ordtbas  20753  ordtrest2  20765  cmpcov2  20950  tgcmp  20961  cmpcld  20962  uncmp  20963  cmpfi  20968  2ndcsep  21019  dis2ndc  21020  restnlly  21042  dislly  21057  comppfsc  21092  kgentopon  21098  kgencmp  21105  kgenidm  21107  iskgen2  21108  kgencn3  21118  ptuni2  21136  ptbasfi  21141  xkouni  21159  txcls  21164  ptclsg  21175  txdis  21192  txindis  21194  txcmplem2  21202  xkopt  21215  txcon  21249  qtopval2  21256  qtopuni  21262  qtoprest  21277  qtopomap  21278  qtopcmap  21279  kqsat  21291  kqcldsat  21293  hmeocls  21328  hmeontr  21329  hmphdis  21356  fgfil  21436  fgabs  21440  trfil1  21447  fgtr  21451  trfg  21452  uzrest  21458  ufilmax  21468  ufileu  21480  filufint  21481  ufildom1  21487  rnelfm  21514  flimfil  21530  uffclsflim  21592  alexsublem  21605  alexsubALTlem3  21610  alexsubALT  21612  ptcmplem2  21614  ptcmplem3  21615  tgpconcompeqg  21672  haustsms2  21697  tgptsmscls  21710  ust0  21780  ustbas2  21786  restutopopn  21799  unirnblps  21981  unirnbl  21982  iccntr  22379  pi1xfrcnv  22612  clsocv  22801  cfilfcls  22824  equivcmet  22866  pjth  22962  hlhil  22966  evthicc2  22980  ovolshft  23030  volsup  23075  dyadmbllem  23117  opnmbllem  23119  mbfconstlem  23146  itg11  23208  limciun  23408  dvidlem  23429  dvnres  23444  cpnord  23448  dvaddf  23455  dvmulf  23456  dvcmulf  23458  dvcof  23461  dvcj  23463  dvrec  23468  dvmptcmul  23477  dvcnv  23488  dvcnvre  23530  ftc1cn  23554  plyco0  23696  taylthlem1  23875  taylthlem2  23876  ulmdvlem3  23904  ulmdv  23905  pserdv  23931  wilthlem2  24539  ppisval  24574  ppisval2  24575  ppinprm  24622  chtnprm  24624  umgraex  25645  ubthlem1  26903  pjhth  27429  ococin  27444  chsupsn  27449  ssjo  27483  chabs1  27552  spansncvi  27688  mdslj1i  28355  mdslj2i  28356  atomli  28418  atcvatlem  28421  atcvat3i  28432  sumdmdlem  28454  reff  29027  cmpcref  29038  xpinpreima2  29074  ordtrest2NEW  29090  sigagenid  29334  imambfm  29444  dya2iocuni  29465  bnj1136  30112  bnj1398  30149  bnj1408  30151  bnj1498  30176  sconpi1  30268  cvmsss2  30303  cvmliftlem15  30327  dftrpred3g  30770  trpredpo  30772  frind  30777  sltval2  30846  nofulllem5  30898  altopthsn  31031  opnbnd  31283  opnregcld  31288  cldregopn  31289  fnessref  31315  neibastop1  31317  topmeet  31322  topjoin  31323  fnemeet1  31324  fnejoin1  31326  bj-restpw  32009  bj-restb  32011  bj-restuni2  32015  dissneqlem  32146  lindsenlbs  32357  poimirlem13  32375  poimirlem14  32376  poimirlem15  32377  opnmbllem0  32398  ftc1cnnc  32437  fdc  32494  sstotbnd2  32526  isbnd2  32535  totbndbnd  32541  prdstotbnd  32546  heibor1  32562  1idl  32778  igenval2  32818  lshpdisj  33075  lssats  33100  lsatcvat3  33140  lkrlsp  33190  lshpset2N  33207  lfl1dim  33209  lfl1dim2N  33210  lkrpssN  33251  paddass  33925  paddidm  33928  pmod1i  33935  pmapjat1  33940  pclbtwnN  33984  pclunN  33985  paddunN  34014  pclfinclN  34037  cdleme50rnlem  34633  dihjust  35307  dihmeetlem1N  35380  dihglblem5apreN  35381  dihmeetlem13N  35409  dochocsp  35469  dochdmj1  35480  dochnoncon  35481  dihjatb  35506  dihjat1lem  35518  lcfl9a  35595  lclkrlem2s  35615  lclkrlem2v  35618  mapdrvallem3  35736  mapdunirnN  35740  mapdin  35752  mapdlsm  35754  baerlem3lem2  35800  baerlem5alem2  35801  baerlem5blem2  35802  hdmaprnN  35957  hgmaprnN  35994  hdmaplkr  36006  rntrclfvOAI  36055  ismrcd1  36062  ismrcd2  36063  isnacs3  36074  nacsfix  36076  kercvrlsm  36454  pwssplit4  36460  hbtlem5  36500  rgspnid  36544  iocinico  36599  mptrcllem  36722  clcnvlem  36732  dmtrcl  36736  rntrcl  36737  cbviuneq12df  36755  dfrcl2  36768  dftrcl3  36814  brtrclfv2  36821  dfrtrcl3  36827  nzin  37322  iunincfi  38083  restuni3  38116  founiiun  38138  founiiun0  38155  disjf1o  38156  inmap  38179  difmapsn  38182  unirnmapsn  38184  iunmapsn  38187  iuneqfzuz  38275  icoiccdif  38380  iccdificc  38396  iooiinicc  38399  icomnfinre  38409  iooiinioc  38413  lptioo2  38481  lptioo1  38482  fourierdlem79  38861  rrxbasefi  38962  qndenserrn  38978  rrxsnicc  38979  intsaluni  39006  issalgend  39015  sge0f1o  39058  iundjiun  39136  meadjiunlem  39141  meaiininclem  39159  caragenuni  39184  caragendifcl  39187  opnvonmbllem2  39306  iinhoiicc  39348  iunhoiioo  39350  pimconstlt1  39375  pimltpnf  39376  pimiooltgt  39381  pimgtmnf2  39384  pimdecfgtioc  39385  pimincfltioc  39386  pimdecfgtioo  39387  pimincfltioo  39388  preimageiingt  39390  preimaleiinlt  39391  sssmf  39408  smflimlem5  39444  smfmullem4  39462  smfpimbor1lem2  39467  fzoopth  40166  upgrex  40299  uvtxnbgr  40608  nbupgruvtxres  40615  cplgruvtxb  40618  cusgredg  40627  lspeqlco  42003
  Copyright terms: Public domain W3C validator