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

Theorem eqssd 3749
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 3747 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3sylanbrc 701 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = 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:  eqrdOLD  3752  uneqdifeq  4189  uneqdifeqOLD  4190  unissel  4608  intmin  4637  unissint  4641  int0el  4648  dmcosseq  5530  sofld  5727  relfld  5810  preddowncl  5856  wfi  5862  tz7.7  5898  fimacnv  6498  knatar  6758  sorpssuni  7099  sorpssint  7100  onint  7148  fo2ndf  7440  suppimacnv  7462  tposeq  7511  wfrlem10  7581  onfununi  7595  tfrlem15  7645  oaass  7798  odi  7816  omass  7817  oelim2  7832  oeeui  7839  nnawordex  7874  oaabslem  7880  oaabs2  7882  omabslem  7883  omabs  7884  uniinqs  7982  sucdom2  8309  fineqv  8328  dffi2  8482  fiuni  8487  dffi3  8490  ordtypelem9  8584  ordtypelem10  8585  oismo  8598  hartogslem1  8600  ixpiunwdom  8649  cantnfp1lem3  8738  oemapvali  8742  cantnf  8751  r1val1  8810  rankval3b  8850  rankunb  8874  rankuni2b  8877  rankr1id  8886  rankc2  8895  rankxplim  8903  tcrank  8908  carden2b  8954  harval2  8984  en2other2  8993  infpwfien  9046  coflim  9246  cfcof  9259  cfidm  9260  isf32lem2  9339  fin1a2lem11  9395  fin1a2lem13  9397  ttukeylem7  9500  fpwwe2  9628  winafp  9682  wuncidm  9731  wuncval2  9732  tskuni  9768  grur1  9805  distrpr  10013  prlem934  10018  ltexpri  10028  reclem4pr  10035  fzopth  12542  fzosplit  12666  fzouzsplit  12668  ccatrn  13532  cotrtrclfv  13923  dmtrclfv  13929  dfrtrcl2  13972  phimullem  15657  prmreclem5  15797  structcnvcnv  16044  imasaddfnlem  16361  imasvscafn  16370  mrcuni  16454  mressmrcd  16460  submrc  16461  ssceq  16658  rescabs  16665  setcepi  16910  clatl  17288  ipopos  17332  psdmrn  17379  psssdm2  17387  dirdm  17406  gsumress  17448  gsumvallem2  17544  gsumwspan  17555  cycsubg  17794  conjnmz  17866  pmtrprfv  18044  symggen  18061  odf1o2  18159  gex1  18177  sylow2alem1  18203  sylow3lem3  18215  lsmidm  18248  lsmss1  18250  lsmss2  18252  lsmmod  18259  lsmdisj  18265  lsmdisj2  18266  cntzcmn  18416  prmcyg  18466  dmdprdd  18569  dprdspan  18597  dprdres  18598  dprdz  18600  subgdmdprd  18604  subgdprd  18605  dprddisj2  18609  dprd2dlem1  18611  dprd2da  18612  dmdprdsplit2lem  18615  dprdsplit  18618  ablfacrp  18636  pgpfac1lem3  18647  kerf1hrm  18916  isdrng2  18930  issubdrg  18978  lspun  19160  lspsn  19175  lspsnneg  19179  lsp0  19182  lsslsp  19188  lmhmlsp  19222  lspextmo  19229  lsmsp  19259  lspprabs  19268  lspsnvs  19287  lspdisj  19298  lsmcv  19314  lspsnat  19318  lsppratlem6  19325  lspprat  19326  lbsextlem4  19334  lidl1el  19391  drngnidl  19402  lidldvgen  19428  fidomndrng  19480  mplbas2  19643  cnsubrg  19979  mulgrhm2  20020  znrrg  20087  ocvin  20191  ocvlsp  20193  mrccss  20211  pjfo  20232  obs2ss  20246  frlmsslsp  20308  topsn  20908  eltg4i  20937  unitg  20944  tgtop  20950  tgidm  20957  en2top  20962  basgen  20965  2basgen  20967  fctop  20981  cctop  20983  ppttop  20984  epttop  20986  ntrin  21038  isopn3  21043  opnnei  21097  neiuni  21099  maxlp  21124  clslp  21125  tgrest  21136  resttopon  21138  rest0  21146  restfpw  21156  restcls  21158  restntr  21159  ordtbas2  21168  ordtbas  21169  ordtrest2  21181  cmpcov2  21366  tgcmp  21377  cmpcld  21378  uncmp  21379  cmpfi  21384  2ndcsep  21435  dis2ndc  21436  restnlly  21458  dislly  21473  comppfsc  21508  kgentopon  21514  kgencmp  21521  kgenidm  21523  iskgen2  21524  kgencn3  21534  ptuni2  21552  ptbasfi  21557  xkouni  21575  txcls  21580  ptclsg  21591  txdis  21608  txindis  21610  txcmplem2  21618  xkopt  21631  txconn  21665  qtopval2  21672  qtopuni  21678  qtoprest  21693  qtopomap  21694  qtopcmap  21695  kqsat  21707  kqcldsat  21709  hmeocls  21744  hmeontr  21745  hmphdis  21772  fgfil  21851  fgabs  21855  trfil1  21862  fgtr  21866  trfg  21867  uzrest  21873  ufilmax  21883  ufileu  21895  filufint  21896  ufildom1  21902  rnelfm  21929  flimfil  21945  uffclsflim  22007  alexsublem  22020  alexsubALTlem3  22025  alexsubALT  22027  ptcmplem2  22029  ptcmplem3  22030  tgpconncompeqg  22087  haustsms2  22112  tgptsmscls  22125  ust0  22195  ustbas2  22201  restutopopn  22214  unirnblps  22396  unirnbl  22397  iccntr  22796  pi1xfrcnv  23028  clsocv  23220  cfilfcls  23243  equivcmet  23285  pjth  23381  hlhil  23385  evthicc2  23400  ovolshft  23450  volsup  23495  dyadmbllem  23538  opnmbllem  23540  mbfconstlem  23566  itg11  23628  limciun  23828  dvidlem  23849  dvnres  23864  cpnord  23868  dvaddf  23875  dvmulf  23876  dvcmulf  23878  dvcof  23881  dvcj  23883  dvrec  23888  dvmptcmul  23897  dvcnv  23910  dvcnvre  23952  ftc1cn  23976  plyco0  24118  taylthlem1  24297  taylthlem2  24298  ulmdvlem3  24326  ulmdv  24327  pserdv  24353  wilthlem2  24965  ppisval  25000  ppisval2  25001  ppinprm  25048  chtnprm  25050  upgrex  26157  uvtxnbgr  26476  nbupgruvtxres  26483  cplgruvtxbOLD  26492  cusgredg  26501  ubthlem1  28006  pjhth  28532  ococin  28547  chsupsn  28552  ssjo  28586  chabs1  28655  spansncvi  28791  mdslj1i  29458  mdslj2i  29459  atomli  29521  atcvatlem  29524  atcvat3i  29535  sumdmdlem  29557  difininv  29632  reff  30186  cmpcref  30197  xpinpreima2  30233  ordtrest2NEW  30249  sigagenid  30494  imambfm  30604  dya2iocuni  30625  reprinfz1  30980  bnj1136  31343  bnj1398  31380  bnj1408  31382  bnj1498  31407  sconnpi1  31499  cvmsss2  31534  cvmliftlem15  31558  dftrpred3g  32009  trpredpo  32011  frpoind  32017  frind  32020  sltval2  32086  noextenddif  32098  scutun12  32194  altopthsn  32345  opnbnd  32597  opnregcld  32602  cldregopn  32603  fnessref  32629  neibastop1  32631  topmeet  32636  topjoin  32637  fnemeet1  32638  fnejoin1  32640  bj-restpw  33322  bj-restb  33324  bj-restuni2  33328  dissneqlem  33469  lindsenlbs  33686  poimirlem13  33704  poimirlem14  33705  poimirlem15  33706  opnmbllem0  33727  ftc1cnnc  33766  fdc  33823  sstotbnd2  33855  isbnd2  33864  totbndbnd  33870  prdstotbnd  33875  heibor1  33891  1idl  34107  igenval2  34147  idreseqidinxp  34373  lshpdisj  34746  lssats  34771  lsatcvat3  34811  lkrlsp  34861  lshpset2N  34878  lfl1dim  34880  lfl1dim2N  34881  lkrpssN  34922  paddass  35596  paddidm  35599  pmod1i  35606  pmapjat1  35611  pclbtwnN  35655  pclunN  35656  paddunN  35685  pclfinclN  35708  cdleme50rnlem  36303  dihjust  36977  dihmeetlem1N  37050  dihglblem5apreN  37051  dihmeetlem13N  37079  dochocsp  37139  dochdmj1  37150  dochnoncon  37151  dihjatb  37176  dihjat1lem  37188  lcfl9a  37265  lclkrlem2s  37285  lclkrlem2v  37288  mapdrvallem3  37406  mapdunirnN  37410  mapdin  37422  mapdlsm  37424  baerlem3lem2  37470  baerlem5alem2  37471  baerlem5blem2  37472  hdmaprnN  37627  hgmaprnN  37664  hdmaplkr  37676  rntrclfvOAI  37725  ismrcd1  37732  ismrcd2  37733  isnacs3  37744  nacsfix  37746  kercvrlsm  38124  pwssplit4  38130  hbtlem5  38169  rgspnid  38213  iocinico  38268  mptrcllem  38391  clcnvlem  38401  dmtrcl  38405  rntrcl  38406  cbviuneq12df  38424  dfrcl2  38437  dftrcl3  38483  brtrclfv2  38490  dfrtrcl3  38496  nzin  38988  iunincfi  39740  restuni3  39769  founiiun  39828  founiiun0  39845  disjf1o  39846  inmap  39869  difmapsn  39872  unirnmapsn  39874  iunmapsn  39877  funimaeq  39929  iuneqfzuz  40018  supminfrnmpt  40139  supminfxr2  40166  supminfxrrnmpt  40168  icoiccdif  40222  iccdificc  40238  iooiinicc  40241  icomnfinre  40251  iooiinioc  40255  lptioo2  40335  lptioo1  40336  limsupresxr  40470  liminfresxr  40471  limsup10exlem  40476  liminfvalxr  40487  fourierdlem79  40874  rrxbasefi  40975  qndenserrn  40991  rrxsnicc  40992  intsaluni  41019  issalgend  41028  sge0f1o  41071  iundjiun  41149  meadjiunlem  41154  meaiininclem  41175  caragenuni  41200  caragendifcl  41203  opnvonmbllem2  41322  iinhoiicc  41363  iunhoiioo  41365  pimconstlt1  41390  pimltpnf  41391  pimiooltgt  41396  pimgtmnf2  41399  pimdecfgtioc  41400  pimincfltioc  41401  pimdecfgtioo  41402  pimincfltioo  41403  preimageiingt  41405  preimaleiinlt  41406  sssmf  41422  smflimlem5  41458  smfmullem4  41476  smfpimbor1lem2  41481  smfsuplem1  41492  fzoopth  41816  sprsymrelf1  42225  lspeqlco  42707  setrecsres  42927
  Copyright terms: Public domain W3C validator