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

Theorem eqssd 3653
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 3651 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3sylanbrc 699 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  eqrdOLD  3656  uneqdifeq  4090  uneqdifeqOLD  4091  unissel  4500  intmin  4529  unissint  4533  int0el  4540  dmcosseq  5419  sofld  5616  relfld  5699  preddowncl  5745  wfi  5751  tz7.7  5787  fimacnv  6387  knatar  6647  sorpssuni  6988  sorpssint  6989  onint  7037  fo2ndf  7329  suppimacnv  7351  tposeq  7399  wfrlem10  7469  onfununi  7483  tfrlem15  7533  oaass  7686  odi  7704  omass  7705  oelim2  7720  oeeui  7727  nnawordex  7762  oaabslem  7768  oaabs2  7770  omabslem  7771  omabs  7772  uniinqs  7870  sucdom2  8197  fineqv  8216  dffi2  8370  fiuni  8375  dffi3  8378  ordtypelem9  8472  ordtypelem10  8473  oismo  8486  hartogslem1  8488  ixpiunwdom  8537  cantnfp1lem3  8615  oemapvali  8619  cantnf  8628  r1val1  8687  rankval3b  8727  rankunb  8751  rankuni2b  8754  rankr1id  8763  rankc2  8772  rankxplim  8780  tcrank  8785  carden2b  8831  harval2  8861  en2other2  8870  infpwfien  8923  coflim  9121  cfcof  9134  cfidm  9135  isf32lem2  9214  fin1a2lem11  9270  fin1a2lem13  9272  ttukeylem7  9375  fpwwe2  9503  winafp  9557  wuncidm  9606  wuncval2  9607  tskuni  9643  grur1  9680  distrpr  9888  prlem934  9893  ltexpri  9903  reclem4pr  9910  fzopth  12416  fzosplit  12540  fzouzsplit  12542  ccatrn  13407  cotrtrclfv  13797  dmtrclfv  13803  dfrtrcl2  13846  phimullem  15531  prmreclem5  15671  structcnvcnv  15918  imasaddfnlem  16235  imasvscafn  16244  mrcuni  16328  mressmrcd  16334  submrc  16335  ssceq  16533  rescabs  16540  setcepi  16785  clatl  17163  ipopos  17207  psdmrn  17254  psssdm2  17262  dirdm  17281  gsumress  17323  gsumvallem2  17419  gsumwspan  17430  cycsubg  17669  conjnmz  17741  pmtrprfv  17919  symggen  17936  odf1o2  18034  gex1  18052  sylow2alem1  18078  sylow3lem3  18090  lsmidm  18123  lsmss1  18125  lsmss2  18127  lsmmod  18134  lsmdisj  18140  lsmdisj2  18141  cntzcmn  18291  prmcyg  18341  dmdprdd  18444  dprdspan  18472  dprdres  18473  dprdz  18475  subgdmdprd  18479  subgdprd  18480  dprddisj2  18484  dprd2dlem1  18486  dprd2da  18487  dmdprdsplit2lem  18490  dprdsplit  18493  ablfacrp  18511  pgpfac1lem3  18522  kerf1hrm  18791  isdrng2  18805  issubdrg  18853  lspun  19035  lspsn  19050  lspsnneg  19054  lsp0  19057  lsslsp  19063  lmhmlsp  19097  lspextmo  19104  lsmsp  19134  lspprabs  19143  lspsnvs  19162  lspdisj  19173  lsmcv  19189  lspsnat  19193  lsppratlem6  19200  lspprat  19201  lbsextlem4  19209  lidl1el  19266  drngnidl  19277  lidldvgen  19303  fidomndrng  19355  mplbas2  19518  cnsubrg  19854  mulgrhm2  19895  znrrg  19962  ocvin  20066  ocvlsp  20068  mrccss  20086  pjfo  20107  obs2ss  20121  frlmsslsp  20183  topsn  20783  eltg4i  20812  unitg  20819  tgtop  20825  tgidm  20832  en2top  20837  basgen  20840  2basgen  20842  fctop  20856  cctop  20858  ppttop  20859  epttop  20861  ntrin  20913  isopn3  20918  opnnei  20972  neiuni  20974  maxlp  20999  clslp  21000  tgrest  21011  resttopon  21013  rest0  21021  restfpw  21031  restcls  21033  restntr  21034  ordtbas2  21043  ordtbas  21044  ordtrest2  21056  cmpcov2  21241  tgcmp  21252  cmpcld  21253  uncmp  21254  cmpfi  21259  2ndcsep  21310  dis2ndc  21311  restnlly  21333  dislly  21348  comppfsc  21383  kgentopon  21389  kgencmp  21396  kgenidm  21398  iskgen2  21399  kgencn3  21409  ptuni2  21427  ptbasfi  21432  xkouni  21450  txcls  21455  ptclsg  21466  txdis  21483  txindis  21485  txcmplem2  21493  xkopt  21506  txconn  21540  qtopval2  21547  qtopuni  21553  qtoprest  21568  qtopomap  21569  qtopcmap  21570  kqsat  21582  kqcldsat  21584  hmeocls  21619  hmeontr  21620  hmphdis  21647  fgfil  21726  fgabs  21730  trfil1  21737  fgtr  21741  trfg  21742  uzrest  21748  ufilmax  21758  ufileu  21770  filufint  21771  ufildom1  21777  rnelfm  21804  flimfil  21820  uffclsflim  21882  alexsublem  21895  alexsubALTlem3  21900  alexsubALT  21902  ptcmplem2  21904  ptcmplem3  21905  tgpconncompeqg  21962  haustsms2  21987  tgptsmscls  22000  ust0  22070  ustbas2  22076  restutopopn  22089  unirnblps  22271  unirnbl  22272  iccntr  22671  pi1xfrcnv  22903  clsocv  23095  cfilfcls  23118  equivcmet  23160  pjth  23256  hlhil  23260  evthicc2  23275  ovolshft  23325  volsup  23370  dyadmbllem  23413  opnmbllem  23415  mbfconstlem  23441  itg11  23503  limciun  23703  dvidlem  23724  dvnres  23739  cpnord  23743  dvaddf  23750  dvmulf  23751  dvcmulf  23753  dvcof  23756  dvcj  23758  dvrec  23763  dvmptcmul  23772  dvcnv  23785  dvcnvre  23827  ftc1cn  23851  plyco0  23993  taylthlem1  24172  taylthlem2  24173  ulmdvlem3  24201  ulmdv  24202  pserdv  24228  wilthlem2  24840  ppisval  24875  ppisval2  24876  ppinprm  24923  chtnprm  24925  upgrex  26032  uvtxnbgr  26351  nbupgruvtxres  26358  cplgruvtxbOLD  26367  cusgredg  26376  ubthlem1  27854  pjhth  28380  ococin  28395  chsupsn  28400  ssjo  28434  chabs1  28503  spansncvi  28639  mdslj1i  29306  mdslj2i  29307  atomli  29369  atcvatlem  29372  atcvat3i  29383  sumdmdlem  29405  difininv  29480  reff  30034  cmpcref  30045  xpinpreima2  30081  ordtrest2NEW  30097  sigagenid  30342  imambfm  30452  dya2iocuni  30473  reprinfz1  30828  bnj1136  31191  bnj1398  31228  bnj1408  31230  bnj1498  31255  sconnpi1  31347  cvmsss2  31382  cvmliftlem15  31406  dftrpred3g  31857  trpredpo  31859  frpoind  31865  frind  31868  sltval2  31934  noextenddif  31946  scutun12  32042  altopthsn  32193  opnbnd  32445  opnregcld  32450  cldregopn  32451  fnessref  32477  neibastop1  32479  topmeet  32484  topjoin  32485  fnemeet1  32486  fnejoin1  32488  bj-restpw  33170  bj-restb  33172  bj-restuni2  33176  dissneqlem  33317  lindsenlbs  33534  poimirlem13  33552  poimirlem14  33553  poimirlem15  33554  opnmbllem0  33575  ftc1cnnc  33614  fdc  33671  sstotbnd2  33703  isbnd2  33712  totbndbnd  33718  prdstotbnd  33723  heibor1  33739  1idl  33955  igenval2  33995  idreseqidinxp  34221  lshpdisj  34592  lssats  34617  lsatcvat3  34657  lkrlsp  34707  lshpset2N  34724  lfl1dim  34726  lfl1dim2N  34727  lkrpssN  34768  paddass  35442  paddidm  35445  pmod1i  35452  pmapjat1  35457  pclbtwnN  35501  pclunN  35502  paddunN  35531  pclfinclN  35554  cdleme50rnlem  36149  dihjust  36823  dihmeetlem1N  36896  dihglblem5apreN  36897  dihmeetlem13N  36925  dochocsp  36985  dochdmj1  36996  dochnoncon  36997  dihjatb  37022  dihjat1lem  37034  lcfl9a  37111  lclkrlem2s  37131  lclkrlem2v  37134  mapdrvallem3  37252  mapdunirnN  37256  mapdin  37268  mapdlsm  37270  baerlem3lem2  37316  baerlem5alem2  37317  baerlem5blem2  37318  hdmaprnN  37473  hgmaprnN  37510  hdmaplkr  37522  rntrclfvOAI  37571  ismrcd1  37578  ismrcd2  37579  isnacs3  37590  nacsfix  37592  kercvrlsm  37970  pwssplit4  37976  hbtlem5  38015  rgspnid  38059  iocinico  38114  mptrcllem  38237  clcnvlem  38247  dmtrcl  38251  rntrcl  38252  cbviuneq12df  38270  dfrcl2  38283  dftrcl3  38329  brtrclfv2  38336  dfrtrcl3  38342  nzin  38834  iunincfi  39586  restuni3  39615  founiiun  39674  founiiun0  39691  disjf1o  39692  inmap  39715  difmapsn  39718  unirnmapsn  39720  iunmapsn  39723  funimaeq  39775  iuneqfzuz  39864  supminfrnmpt  39985  supminfxr2  40012  supminfxrrnmpt  40014  icoiccdif  40068  iccdificc  40084  iooiinicc  40087  icomnfinre  40097  iooiinioc  40101  lptioo2  40181  lptioo1  40182  limsupresxr  40316  liminfresxr  40317  limsup10exlem  40322  liminfvalxr  40333  fourierdlem79  40720  rrxbasefi  40821  qndenserrn  40837  rrxsnicc  40838  intsaluni  40865  issalgend  40874  sge0f1o  40917  iundjiun  40995  meadjiunlem  41000  meaiininclem  41021  caragenuni  41046  caragendifcl  41049  opnvonmbllem2  41168  iinhoiicc  41209  iunhoiioo  41211  pimconstlt1  41236  pimltpnf  41237  pimiooltgt  41242  pimgtmnf2  41245  pimdecfgtioc  41246  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  preimageiingt  41251  preimaleiinlt  41252  sssmf  41268  smflimlem5  41304  smfmullem4  41322  smfpimbor1lem2  41327  smfsuplem1  41338  fzoopth  41662  sprsymrelf1  42071  lspeqlco  42553  setrecsres  42773
  Copyright terms: Public domain W3C validator