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

Theorem eqssd 3966
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 3964 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3sylanbrc 584 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  eqelssd  3970  uneqdifeq  4455  pweq  4579  unieq  4881  unissel  4904  intmin  4934  unissint  4938  int0el  4945  intidg  5419  dmcosseq  5933  sofld  6144  relfld  6232  preddowncl  6291  frpoind  6301  wfiOLD  6310  tz7.7  6348  fimacnvOLD  7026  knatar  7307  sorpssuni  7674  sorpssint  7675  onint  7730  fo2ndf  8058  suppimacnv  8110  tposeq  8164  frrlem14  8235  onfununi  8292  tfrlem15  8343  oaass  8513  odi  8531  omass  8532  oelim2  8547  oeeui  8554  nnawordex  8589  oaabslem  8598  oaabs2  8600  omabslem  8601  omabs  8602  cofon1  8623  uniinqs  8743  sucdom2OLD  9033  sucdom2  9157  onomeneq  9179  fineqv  9214  dffi2  9366  fiuni  9371  dffi3  9374  hartogslem1  9485  ixpiunwdom  9533  cantnfp1lem3  9623  oemapvali  9627  cantnf  9636  dfttrcl2  9667  frind  9693  r1val1  9729  rankval3b  9769  rankunb  9793  rankuni2b  9796  rankr1id  9805  rankc2  9814  rankxplim  9822  tcrank  9827  carden2b  9910  harval2  9940  en2other2  9952  infpwfien  10005  coflim  10204  cfcof  10217  cfidm  10218  isf32lem2  10297  fin1a2lem11  10353  fin1a2lem13  10355  ttukeylem7  10458  fpwwe2  10586  winafp  10640  wuncidm  10689  wuncval2  10690  tskuni  10726  grur1  10763  distrpr  10971  ltexpri  10986  reclem4pr  10993  fzopth  13485  fzosplit  13612  fzouzsplit  13614  ccatrn  14484  cotrtrclfv  14904  dmtrclfv  14910  dfrtrcl2  14954  structcnvcnv  17032  imasaddfnlem  17417  imasvscafn  17426  mrcuni  17508  mressmrcd  17514  submrc  17515  ssceq  17716  rescabs  17725  rescabsOLD  17726  setcepi  17981  clatl  18404  ipopos  18432  psdmrn  18469  dirdm  18496  gsumress  18544  gsumvallem2  18651  gsumwspan  18663  trivsubgd  18962  trivsubgsnd  18963  trivnsgd  18981  cycsubg  19008  conjnmz  19049  pmtrprfv  19242  symggen  19259  odf1o2  19362  gex1  19380  sylow2alem1  19406  smndlsmidm  19445  lsmss1  19454  lsmss2  19456  lsmmod  19464  lsmdisj  19470  lsmdisj2  19471  cntzcmn  19625  prmcyg  19678  dmdprdd  19785  dprdspan  19813  dprdres  19814  dprdz  19816  subgdmdprd  19820  subgdprd  19821  dprddisj2  19825  dprd2dlem1  19827  dprd2da  19828  dmdprdsplit2lem  19831  dprdsplit  19834  ablfacrp  19852  pgpfac1lem3  19863  kerf1ghm  20186  issubdrg  20263  lspun  20464  lspsn  20479  lspsnneg  20483  lsp0  20486  lsslsp  20492  lmhmlsp  20526  lspextmo  20533  lsmsp  20563  lspprabs  20572  lspsnvs  20591  lspdisj  20602  lsmcv  20618  lspsnat  20622  lsppratlem6  20629  lspprat  20630  lbsextlem4  20638  lidl1el  20704  drngnidl  20715  lidldvgen  20741  cnsubrg  20873  mulgrhm2  20915  znrrg  20988  ocvin  21094  ocvlsp  21096  mrccss  21114  topsn  22296  eltg4i  22326  unitg  22333  tgtop  22339  tgidm  22346  en2top  22351  basgen  22354  2basgen  22356  fctop  22370  cctop  22372  ppttop  22373  epttop  22375  ntrin  22428  isopn3  22433  opnnei  22487  neiuni  22489  maxlp  22514  clslp  22515  tgrest  22526  resttopon  22528  rest0  22536  restcls  22548  restntr  22549  ordtbas2  22558  ordtbas  22559  ordtrest2  22571  cmpcov2  22757  tgcmp  22768  cmpcld  22769  uncmp  22770  cmpfi  22775  dis2ndc  22827  restnlly  22849  dislly  22864  comppfsc  22899  kgentopon  22905  kgencmp  22912  kgenidm  22914  iskgen2  22915  kgencn3  22925  ptuni2  22943  ptbasfi  22948  xkouni  22966  txcls  22971  txdis  22999  txindis  23001  txcmplem2  23009  xkopt  23022  txconn  23056  qtopval2  23063  qtopuni  23069  qtoprest  23084  qtopomap  23085  qtopcmap  23086  kqsat  23098  kqcldsat  23100  hmeocls  23135  hmeontr  23136  hmphdis  23163  fgfil  23242  fgabs  23246  trfil1  23253  fgtr  23257  uzrest  23264  ufilmax  23274  ufileu  23286  filufint  23287  ufildom1  23293  rnelfm  23320  flimfil  23336  uffclsflim  23398  alexsublem  23411  alexsubALTlem3  23416  alexsubALT  23418  ptcmplem2  23420  ptcmplem3  23421  tgpconncompeqg  23479  haustsms2  23504  tgptsmscls  23517  ust0  23587  ustbas2  23593  iccntr  24200  pi1xfrcnv  24436  clsocv  24630  cfilfcls  24654  equivcmet  24697  hlhil  24823  evthicc2  24840  ovolshft  24891  volsup  24936  dyadmbllem  24979  mbfconstlem  25007  itg11  25071  limciun  25274  dvnres  25311  cpnord  25315  dvcmulf  25325  dvmptcmul  25344  dvcnvre  25399  plyco0  25569  taylthlem1  25748  taylthlem2  25749  ulmdvlem3  25777  wilthlem2  26434  ppisval  26469  ppinprm  26517  chtnprm  26519  sltval2  27020  noextenddif  27032  scutun12  27171  madebdaylemlrcut  27250  cofcut1  27261  upgrex  28085  uvtxnbgr  28390  cusgredg  28414  ubthlem1  29854  pjhth  30377  ococin  30392  chsupsn  30397  ssjo  30431  chabs1  30500  spansncvi  30636  mdslj1i  31303  mdslj2i  31304  atomli  31366  atcvatlem  31369  atcvat3i  31380  sumdmdlem  31402  difininv  31486  fnpreimac  31629  pmtrcnelor  31984  cycpmrn  32034  fldgenid  32126  1fldgenq  32129  rspidlid  32203  0ringidl  32242  dimkerim  32362  cmpcref  32471  zarcls1  32490  zarclssn  32494  zart0  32500  zarcmplem  32502  xpinpreima2  32528  ordtrest2NEW  32544  sigagenid  32790  imambfm  32902  reprinfz1  33275  bnj1136  33649  bnj1398  33686  bnj1408  33688  bnj1498  33713  fineqvacALT  33739  sconnpi1  33873  cvmliftlem15  33932  altopthsn  34575  opnbnd  34826  opnregcld  34831  cldregopn  34832  fnessref  34858  neibastop1  34860  topmeet  34865  topjoin  34866  fnemeet1  34867  fnejoin1  34869  bj-gabeqd  35436  bj-restpw  35592  bj-restb  35594  bj-restuni2  35598  dissneqlem  35840  pibt2  35917  lindsenlbs  36102  poimirlem13  36120  poimirlem14  36121  poimirlem15  36122  fdc  36233  sstotbnd2  36262  isbnd2  36271  totbndbnd  36277  prdstotbnd  36282  heibor1  36298  1idl  36514  igenval2  36554  idreseqidinxp  36799  disjdmqs  37295  lshpdisj  37478  lssats  37503  lsatcvat3  37543  lshpset2N  37610  lfl1dim  37612  lfl1dim2N  37613  lkrpssN  37654  paddass  38330  paddidm  38333  pmod1i  38340  pmapjat1  38345  pclbtwnN  38389  pclunN  38390  paddunN  38419  pclfinclN  38442  dihjust  39709  dihmeetlem1N  39782  dihglblem5apreN  39783  dihmeetlem13N  39811  dochocsp  39871  dochdmj1  39882  dochnoncon  39883  dihjatb  39908  dihjat1lem  39920  lcfl9a  39997  lclkrlem2s  40017  lclkrlem2v  40020  mapdrvallem3  40138  mapdunirnN  40142  mapdin  40154  mapdlsm  40156  baerlem3lem2  40202  baerlem5alem2  40203  baerlem5blem2  40204  hdmaplkr  40405  sticksstones11  40593  rntrclfvOAI  41043  ismrcd1  41050  ismrcd2  41051  isnacs3  41062  nacsfix  41064  rgspnid  41528  iocinico  41575  onsupmaxb  41602  onsssupeqcond  41644  oacl2g  41694  omabs2  41696  omcl2  41697  ofoaf  41700  onsucunifi  41715  naddwordnexlem4  41747  harval3  41884  mptrcllem  41959  clcnvlem  41969  dmtrcl  41973  rntrcl  41974  cbviuneq12df  42007  dfrcl2  42020  dftrcl3  42066  brtrclfv2  42073  dfrtrcl3  42079  scottrankd  42602  nzin  42672  iunincfi  43378  founiiun  43470  founiiun0  43483  inmap  43504  difmapsn  43507  funimaeq  43548  iuneqfzuz  43643  supminfrnmpt  43754  supminfxr2  43778  supminfxrrnmpt  43780  pimxrneun  43798  iooiinicc  43854  icomnfinre  43864  iooiinioc  43868  limsupresxr  44081  liminfresxr  44082  limsup10exlem  44087  liminfvalxr  44098  fourierdlem79  44500  rrxsnicc  44615  prsal  44633  issalgend  44653  sge0f1o  44697  caragenuni  44826  caragendifcl  44829  opnvonmbllem2  44948  iinhoiicc  44989  pimconstlt1  45017  pimltpnff  45018  pimiooltgt  45025  pimgtmnf2  45029  pimdecfgtioc  45030  pimincfltioc  45031  pimdecfgtioo  45032  pimincfltioo  45033  preimageiingt  45035  preimaleiinlt  45036  pimgtmnff  45037  sssmf  45053  smflimlem5  45090  smfmullem4  45109  smfpimbor1lem2  45114  smfsuplem1  45126  smfpimne2  45155  fsupdm  45157  finfdm  45161  fzoopth  45633  sprsymrelf1  45762  lspeqlco  46594  isclatd  47082  intubeu  47083  unilbeu  47084  setrecsres  47221
  Copyright terms: Public domain W3C validator