MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqrdv Unicode version

Theorem eqrdv 2454
Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
Hypothesis
Ref Expression
eqrdv.1
Assertion
Ref Expression
eqrdv
Distinct variable groups:   ,   ,   ,

Proof of Theorem eqrdv
StepHypRef Expression
1 eqrdv.1 . . 3
21alrimiv 1719 . 2
3 dfcleq 2450 . 2
42, 3sylibr 212 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  =wceq 1395  e.wcel 1818
This theorem is referenced by:  eqrdav  2455  eqrdavOLD  2456  uneq1  3650  ineq1  3692  unineq  3747  difin2  3759  csbcomgOLD  3838  csbabgOLD  3856  difsn  4164  intmin4  4316  iunconst  4339  iinconst  4340  dfiun2g  4362  iindif2  4399  iinin2  4400  iunxsng  4409  opthprc  5052  inimasn  5428  dmsnopg  5484  dfco2a  5512  iotaeq  5564  imadif  5668  ssimaex  5938  unpreima  6013  respreima  6016  iinpreima  6017  fnsnb  6090  fmptsng  6092  fmptsnd  6093  fconstfvOLD  6134  iunpw  6614  ordpwsuc  6650  ordsucun  6660  fun11iun  6760  reldm  6851  rntpos  6987  onoviun  7033  oarec  7230  iserd  7356  erth  7375  map0e  7476  ixpiin  7515  boxriin  7531  pw2f1olem  7641  fifo  7912  ordiso2  7961  finacn  8452  acnen  8455  acacni  8541  dfac13  8543  fin23lem26  8726  isf34lem4  8778  axdc3lem2  8852  fpwwe2lem8  9036  fpwwe2lem12  9040  fpwwe2lem13  9041  gch2  9074  gchac  9080  gchina  9098  genpass  9408  1idpr  9428  eqreznegel  11196  ixxun  11574  iccid  11603  difreicc  11681  iccsplit  11682  fzsplit2  11739  fzsn  11754  fzpr  11764  uzsplit  11779  fz1isolem  12510  pr2pwpr  12520  isercolllem2  13488  isercoll  13490  bitsmod  14086  bitscmp  14088  saddisj  14115  sadadd  14117  sadass  14121  smupvallem  14133  smueqlem  14140  smumul  14143  gcdcllem2  14150  vdwapun  14492  firest  14830  mhmpropd  15972  subgacs  16236  eqgid  16253  ghmmhmb  16278  ghmpropd  16304  resscntz  16369  symg1bas  16421  lsmcom2  16675  lsmass  16688  ablnsg  16853  lsmcomx  16862  gsum2d2  17002  subgdmdprd  17081  dprd2d2  17093  unitpropd  17346  subsubrg2  17456  subrgpropd  17463  rhmpropd  17464  abvpropd  17491  lssacs  17613  lssats2  17646  lsspropd  17663  lmhmpropd  17719  lbspropd  17745  unitgOLD  19469  discld  19590  neiptopnei  19633  neiptopreu  19634  restsn  19671  restdis  19679  neitr  19681  restlp  19684  cndis  19792  cnindis  19793  cnpdis  19794  lpcls  19865  hausmapdom  20001  ptpjpre1  20072  tx1cn  20110  tx2cn  20111  hauseqlcld  20147  txkgen  20153  idqtop  20207  tgqtop  20213  acufl  20418  uffix  20422  ufildr  20432  fmfg  20450  rnelfm  20454  fmfnfm  20459  fmid  20461  fmco  20462  flimrest  20484  fclsrest  20525  alexsubALT  20551  tsmsgsum  20637  tsmsgsumOLD  20640  tsmssubm  20644  tsmsresOLD  20645  tsmsres  20646  tsmsf1o  20647  xpsdsval  20884  blpnf  20900  blin  20924  blres  20934  xmetec  20937  imasf1obl  20991  imasf1oxms  20992  prdsbl  20994  metrest  21027  metutopOLD  21085  psmetutop  21086  restmetu  21090  dscopn  21094  cnbl0  21281  bl2ioo  21297  xrtgioo  21311  cncfmet  21412  icoopnst  21439  iocopnst  21440  cldcss2  21857  iunmbl2  21967  mbfmulc2lem  22054  mbfmax  22056  ismbf3d  22061  mbfimaopnlem  22062  mbfaddlem  22067  mbfsup  22071  i1f1lem  22096  i1faddlem  22100  i1fmullem  22101  i1fmulclem  22109  i1fres  22112  mbfi1fseqlem4  22125  limcdif  22280  limcnlp  22282  limcflf  22285  limcres  22290  limcun  22299  ply1remlem  22563  fta1glem2  22567  plypf1  22609  ofmulrt  22678  plyremlem  22700  aannenlem1  22724  tglineelsb2  24012  tglinecom  24015  cusgrarn  24459  uvtxnbgra  24493  clwwlknscsh  24819  2wot2wont  24886  2spot2iun2spont  24891  nbhashuvtx  24916  vdiscusgra  24921  rusgranumwlkb0  24953  eupath2  24980  usg2spot2nb  25065  usgreg2spot  25067  numclwwlkun  25079  ubthlem1  25786  ocin  26214  shscom  26237  spansncol  26486  unipreima  27484  1stpreima  27524  2ndpreima  27525  fpwrelmapffslem  27555  iocinioc2  27590  nndiffz1  27596  fzsplit3  27599  fimaproj  27836  qtophaus  27839  locfinreflem  27843  prsdm  27896  prsrn  27897  indpi1  28035  indf1ofs  28039  1stmbfm  28231  2ndmbfm  28232  mbfmcnt  28239  eulerpartlemgh  28317  dstfrvunirn  28413  preduz  29280  predfz  29283  ontgval  29896  heicant  30049  neifg  30189  filnetlem4  30199  istotbnd3  30267  sstotbnd  30271  ismtyima  30299  heibor  30317  divrngidl  30425  prtlem19  30619  prter2  30622  mzpmfp  30679  mzpmfpOLD  30680  lzunuz  30701  fz1eqin  30702  jm2.23  30938  pw2f1ocnv  30979  dfacbasgrp  31057  subrgacs  31149  sdrgacs  31150  rfcnpre3  31408  rfcnpre4  31409  unima  31441  iccshift  31558  iocopn  31560  iooshift  31562  iccintsng  31563  icoopn  31565  limcdm0  31624  limcresiooub  31648  limcresioolb  31649  fperdvper  31715  itgperiod  31780  fourierdlem32  31921  fourierdlem33  31922  fourierdlem48  31937  fourierdlem49  31938  fourierdlem81  31970  mgmhmpropd  32473  tpres  32554  fncnvimaeqv  32626  rnghmval2  32701  lkrsc  34822  lshpkr  34842  paddvaln0N  35525  paddval0  35534  diaglbN  36782  cdlemm10N  36845  lcfrvalsnN  37268  lcfrlem9  37277  lcdlss  37346  mapd1o  37375  mapd0  37392  hlhillcs  37688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449
  Copyright terms: Public domain W3C validator