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

Theorem eqssd 3612
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 3610 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3sylanbrc 697 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581
This theorem is referenced by:  eqrdOLD  3615  uneqdifeq  4048  uneqdifeqOLD  4049  unissel  4459  intmin  4488  unissint  4492  int0el  4499  dmcosseq  5376  sofld  5569  relfld  5649  preddowncl  5695  wfi  5701  tz7.7  5737  fimacnv  6333  knatar  6592  sorpssuni  6931  sorpssint  6932  onint  6980  fo2ndf  7269  suppimacnv  7291  tposeq  7339  wfrlem10  7409  onfununi  7423  tfrlem15  7473  oaass  7626  odi  7644  omass  7645  oelim2  7660  oeeui  7667  nnawordex  7702  oaabslem  7708  oaabs2  7710  omabslem  7711  omabs  7712  uniinqs  7812  sucdom2  8141  fineqv  8160  dffi2  8314  fiuni  8319  dffi3  8322  ordtypelem9  8416  ordtypelem10  8417  oismo  8430  hartogslem1  8432  ixpiunwdom  8481  cantnfp1lem3  8562  oemapvali  8566  cantnf  8575  r1val1  8634  rankval3b  8674  rankunb  8698  rankuni2b  8701  rankr1id  8710  rankc2  8719  rankxplim  8727  tcrank  8732  carden2b  8778  harval2  8808  en2other2  8817  infpwfien  8870  coflim  9068  cfcof  9081  cfidm  9082  isf32lem2  9161  fin1a2lem11  9217  fin1a2lem13  9219  ttukeylem7  9322  fpwwe2  9450  winafp  9504  wuncidm  9553  wuncval2  9554  tskuni  9590  grur1  9627  distrpr  9835  prlem934  9840  ltexpri  9850  reclem4pr  9857  fzopth  12363  fzosplit  12485  fzouzsplit  12487  ccatrn  13355  cotrtrclfv  13734  dmtrclfv  13740  dfrtrcl2  13783  phimullem  15465  prmreclem5  15605  structcnvcnv  15852  imasaddfnlem  16169  imasvscafn  16178  mrcuni  16262  mressmrcd  16268  submrc  16269  ssceq  16467  rescabs  16474  setcepi  16719  clatl  17097  ipopos  17141  psdmrn  17188  psssdm2  17196  dirdm  17215  gsumress  17257  gsumvallem2  17353  gsumwspan  17364  cycsubg  17603  conjnmz  17675  pmtrprfv  17854  symggen  17871  odf1o2  17969  gex1  17987  sylow2alem1  18013  sylow3lem3  18025  lsmidm  18058  lsmss1  18060  lsmss2  18062  lsmmod  18069  lsmdisj  18075  lsmdisj2  18076  cntzcmn  18226  prmcyg  18276  dmdprdd  18379  dprdspan  18407  dprdres  18408  dprdz  18410  subgdmdprd  18414  subgdprd  18415  dprddisj2  18419  dprd2dlem1  18421  dprd2da  18422  dmdprdsplit2lem  18425  dprdsplit  18428  ablfacrp  18446  pgpfac1lem3  18457  kerf1hrm  18724  isdrng2  18738  issubdrg  18786  lspun  18968  lspsn  18983  lspsnneg  18987  lsp0  18990  lsslsp  18996  lmhmlsp  19030  lspextmo  19037  lsmsp  19067  lspprabs  19076  lspsnvs  19095  lspdisj  19106  lsmcv  19122  lspsnat  19126  lsppratlem6  19133  lspprat  19134  lbsextlem4  19142  lidl1el  19199  drngnidl  19210  lidldvgen  19236  fidomndrng  19288  mplbas2  19451  cnsubrg  19787  mulgrhm2  19828  znrrg  19895  ocvin  19999  ocvlsp  20001  mrccss  20019  pjfo  20040  obs2ss  20054  frlmsslsp  20116  topsn  20716  eltg4i  20745  unitg  20752  tgtop  20758  tgidm  20765  en2top  20770  basgen  20773  2basgen  20775  fctop  20789  cctop  20791  ppttop  20792  epttop  20794  ntrin  20846  isopn3  20851  opnnei  20905  neiuni  20907  maxlp  20932  clslp  20933  tgrest  20944  resttopon  20946  rest0  20954  restfpw  20964  restcls  20966  restntr  20967  ordtbas2  20976  ordtbas  20977  ordtrest2  20989  cmpcov2  21174  tgcmp  21185  cmpcld  21186  uncmp  21187  cmpfi  21192  2ndcsep  21243  dis2ndc  21244  restnlly  21266  dislly  21281  comppfsc  21316  kgentopon  21322  kgencmp  21329  kgenidm  21331  iskgen2  21332  kgencn3  21342  ptuni2  21360  ptbasfi  21365  xkouni  21383  txcls  21388  ptclsg  21399  txdis  21416  txindis  21418  txcmplem2  21426  xkopt  21439  txconn  21473  qtopval2  21480  qtopuni  21486  qtoprest  21501  qtopomap  21502  qtopcmap  21503  kqsat  21515  kqcldsat  21517  hmeocls  21552  hmeontr  21553  hmphdis  21580  fgfil  21660  fgabs  21664  trfil1  21671  fgtr  21675  trfg  21676  uzrest  21682  ufilmax  21692  ufileu  21704  filufint  21705  ufildom1  21711  rnelfm  21738  flimfil  21754  uffclsflim  21816  alexsublem  21829  alexsubALTlem3  21834  alexsubALT  21836  ptcmplem2  21838  ptcmplem3  21839  tgpconncompeqg  21896  haustsms2  21921  tgptsmscls  21934  ust0  22004  ustbas2  22010  restutopopn  22023  unirnblps  22205  unirnbl  22206  iccntr  22605  pi1xfrcnv  22838  clsocv  23030  cfilfcls  23053  equivcmet  23095  pjth  23191  hlhil  23195  evthicc2  23210  ovolshft  23260  volsup  23305  dyadmbllem  23348  opnmbllem  23350  mbfconstlem  23377  itg11  23439  limciun  23639  dvidlem  23660  dvnres  23675  cpnord  23679  dvaddf  23686  dvmulf  23687  dvcmulf  23689  dvcof  23692  dvcj  23694  dvrec  23699  dvmptcmul  23708  dvcnv  23721  dvcnvre  23763  ftc1cn  23787  plyco0  23929  taylthlem1  24108  taylthlem2  24109  ulmdvlem3  24137  ulmdv  24138  pserdv  24164  wilthlem2  24776  ppisval  24811  ppisval2  24812  ppinprm  24859  chtnprm  24861  upgrex  25968  uvtxnbgr  26282  nbupgruvtxres  26289  cplgruvtxb  26292  cusgredg  26301  ubthlem1  27696  pjhth  28222  ococin  28237  chsupsn  28242  ssjo  28276  chabs1  28345  spansncvi  28481  mdslj1i  29148  mdslj2i  29149  atomli  29211  atcvatlem  29214  atcvat3i  29225  sumdmdlem  29247  difininv  29326  reff  29880  cmpcref  29891  xpinpreima2  29927  ordtrest2NEW  29943  sigagenid  30188  imambfm  30298  dya2iocuni  30319  reprinfz1  30674  bnj1136  31039  bnj1398  31076  bnj1408  31078  bnj1498  31103  sconnpi1  31195  cvmsss2  31230  cvmliftlem15  31254  dftrpred3g  31707  trpredpo  31709  frind  31714  sltval2  31783  noextenddif  31795  scutun12  31891  altopthsn  32043  opnbnd  32295  opnregcld  32300  cldregopn  32301  fnessref  32327  neibastop1  32329  topmeet  32334  topjoin  32335  fnemeet1  32336  fnejoin1  32338  bj-restpw  33020  bj-restb  33022  bj-restuni2  33026  dissneqlem  33158  lindsenlbs  33375  poimirlem13  33393  poimirlem14  33394  poimirlem15  33395  opnmbllem0  33416  ftc1cnnc  33455  fdc  33512  sstotbnd2  33544  isbnd2  33553  totbndbnd  33559  prdstotbnd  33564  heibor1  33580  1idl  33796  igenval2  33836  lshpdisj  34093  lssats  34118  lsatcvat3  34158  lkrlsp  34208  lshpset2N  34225  lfl1dim  34227  lfl1dim2N  34228  lkrpssN  34269  paddass  34943  paddidm  34946  pmod1i  34953  pmapjat1  34958  pclbtwnN  35002  pclunN  35003  paddunN  35032  pclfinclN  35055  cdleme50rnlem  35651  dihjust  36325  dihmeetlem1N  36398  dihglblem5apreN  36399  dihmeetlem13N  36427  dochocsp  36487  dochdmj1  36498  dochnoncon  36499  dihjatb  36524  dihjat1lem  36536  lcfl9a  36613  lclkrlem2s  36633  lclkrlem2v  36636  mapdrvallem3  36754  mapdunirnN  36758  mapdin  36770  mapdlsm  36772  baerlem3lem2  36818  baerlem5alem2  36819  baerlem5blem2  36820  hdmaprnN  36975  hgmaprnN  37012  hdmaplkr  37024  rntrclfvOAI  37073  ismrcd1  37080  ismrcd2  37081  isnacs3  37092  nacsfix  37094  kercvrlsm  37472  pwssplit4  37478  hbtlem5  37517  rgspnid  37561  iocinico  37616  mptrcllem  37739  clcnvlem  37749  dmtrcl  37753  rntrcl  37754  cbviuneq12df  37772  dfrcl2  37785  dftrcl3  37831  brtrclfv2  37838  dfrtrcl3  37844  nzin  38337  iunincfi  39092  restuni3  39121  founiiun  39176  founiiun0  39193  disjf1o  39194  inmap  39217  difmapsn  39220  unirnmapsn  39222  iunmapsn  39225  funimaeq  39277  iuneqfzuz  39364  supminfrnmpt  39485  supminfxr2  39512  supminfxrrnmpt  39514  icoiccdif  39553  iccdificc  39569  iooiinicc  39572  icomnfinre  39582  iooiinioc  39586  lptioo2  39663  lptioo1  39664  limsupresxr  39792  liminfresxr  39793  limsup10exlem  39798  liminfvalxr  39809  fourierdlem79  40165  rrxbasefi  40266  qndenserrn  40282  rrxsnicc  40283  intsaluni  40310  issalgend  40319  sge0f1o  40362  iundjiun  40440  meadjiunlem  40445  meaiininclem  40463  caragenuni  40488  caragendifcl  40491  opnvonmbllem2  40610  iinhoiicc  40651  iunhoiioo  40653  pimconstlt1  40678  pimltpnf  40679  pimiooltgt  40684  pimgtmnf2  40687  pimdecfgtioc  40688  pimincfltioc  40689  pimdecfgtioo  40690  pimincfltioo  40691  preimageiingt  40693  preimaleiinlt  40694  sssmf  40710  smflimlem5  40746  smfmullem4  40764  smfpimbor1lem2  40769  smfsuplem1  40780  fzoopth  41100  sprsymrelf1  41511  lspeqlco  41993
  Copyright terms: Public domain W3C validator