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

Theorem eqrdv 2823
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 1921 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfcleq 2819 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 235 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1528   = wceq 1530  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2818
This theorem is referenced by:  eqrdav  2824  abbi1  2888  abbi2dv  2954  uneq1  4135  ineq1OLD  4185  unineq  4257  difin2  4269  difsn  4729  intmin4  4902  iunconst  4925  iinconst  4926  dfiun2g  4951  dfiun2gOLD  4952  iindif1  4993  iindif2  4995  iinin2  4996  iunxsng  5008  iunxsngf  5010  opthprc  5614  dmopab2rex  5784  inimasn  6010  dmsnopg  6067  dfco2a  6096  iotaeq  6323  imadif  6434  unima  6735  ssimaex  6744  unpreima  6828  respreima  6831  iinpreima  6832  fnsnb  6923  fmptsng  6925  fmptsnd  6926  tpres  6962  iunpw  7484  ordpwsuc  7521  ordsucun  7531  fiunw  7635  f1iunw  7636  fiun  7638  f1iun  7639  reldm  7737  fimaproj  7823  rntpos  7899  onoviun  7974  oarec  8181  iserd  8308  erth  8331  mapdm0  8414  ixpiin  8480  boxriin  8496  pw2f1olem  8613  fifo  8888  ordiso2  8971  finacn  9468  acnen  9471  acacni  9558  dfac13  9560  fin23lem26  9739  isf34lem4  9791  axdc3lem2  9865  fpwwe2lem8  10051  fpwwe2lem12  10055  fpwwe2lem13  10056  gch2  10089  gchac  10095  gchina  10113  genpass  10423  1idpr  10443  eqreznegel  12326  ixxun  12747  iccid  12776  difreicc  12863  iccsplit  12864  fzsplit2  12925  fzsn  12942  fzpr  12955  uzsplit  12972  preduz  13022  predfz  13025  fz1isolem  13812  pr2pwpr  13830  isercolllem2  15015  isercoll  15017  bitsmod  15777  bitscmp  15779  saddisj  15806  sadadd  15808  sadass  15812  smupvallem  15824  smueqlem  15831  smumul  15834  gcdcllem2  15841  vdwapun  16302  firest  16698  fncnvimaeqv  17362  mhmpropd  17952  subgacs  18245  eqgid  18264  ghmmhmb  18301  ghmpropd  18328  resscntz  18394  symg1bas  18446  lsmcom2  18702  lsmass  18717  ablnsg  18889  lsmcomx  18898  gsum2d2  19016  subgdmdprd  19078  dprd2d2  19088  2nsgsimpgd  19146  unitpropd  19369  subsubrg2  19484  subrgpropd  19492  rhmpropd  19493  subrgacs  19501  sdrgacs  19502  abvpropd  19535  lssacs  19661  lssats2  19694  lsspropd  19711  lmhmpropd  19767  lbspropd  19793  discld  21613  neiptopnei  21656  neiptopreu  21657  restsn  21694  restdis  21702  neitr  21704  restlp  21707  cndis  21815  cnindis  21816  cnpdis  21817  lpcls  21888  hausmapdom  22024  ptpjpre1  22095  tx1cn  22133  tx2cn  22134  hauseqlcld  22170  txkgen  22176  idqtop  22230  tgqtop  22236  acufl  22441  uffix  22445  ufildr  22455  fmfg  22473  rnelfm  22477  fmfnfm  22482  fmid  22484  fmco  22485  flimrest  22507  fclsrest  22548  alexsubALT  22575  tsmsgsum  22662  tsmssubm  22666  tsmsres  22667  tsmsf1o  22668  xpsdsval  22906  blpnf  22922  blin  22946  blres  22956  xmetec  22959  imasf1obl  23013  imasf1oxms  23014  prdsbl  23016  metrest  23049  psmetutop  23092  restmetu  23095  dscopn  23098  cnbl0  23297  bl2ioo  23315  xrtgioo  23329  cncfmet  23431  icoopnst  23458  iocopnst  23459  cldcss2  23960  iunmbl2  24073  mbfmulc2lem  24163  mbfmax  24165  ismbf3d  24170  mbfimaopnlem  24171  mbfaddlem  24176  mbfsup  24180  i1f1lem  24205  i1faddlem  24209  i1fmullem  24210  i1fmulclem  24218  i1fres  24221  mbfi1fseqlem4  24234  limcdif  24389  limcnlp  24391  limcflf  24394  limcres  24399  limcun  24408  ply1remlem  24671  fta1glem2  24675  plypf1  24717  ofmulrt  24786  plyremlem  24808  aannenlem1  24832  gausslemma2dlem1a  25855  tglineelsb2  26332  tglinecom  26335  ushgredgedg  26925  ushgredgedgloop  26927  nbumgrvtx  27042  nbusgrvtxm1uvtx  27101  vdiscusgr  27227  wspniunwspnon  27616  rusgrnumwwlkb0  27664  clwwlknscsh  27755  clwwlknun  27805  eupth2lems  27931  fusgr2wsp2nb  28027  fusgreg2wsp  28029  ubthlem1  28561  ocin  28987  shscom  29010  spansncol  29259  eqsnd  30203  iunsnima  30284  nfpconfp  30292  unipreima  30306  1stpreimas  30354  1stpreima  30355  2ndpreima  30356  fpwrelmapffslem  30381  iocinioc2  30415  nndiffz1  30422  fzsplit3  30430  swrdrn3  30543  cntzun  30609  cntzsnid  30610  ecxpid  30839  qsxpid  30841  lindspropd  30857  smatrcl  30947  qtophaus  30986  locfinreflem  30990  prsdm  31043  prsrn  31044  indpi1  31165  indf1ofs  31171  1stmbfm  31404  2ndmbfm  31405  mbfmcnt  31412  eulerpartlemgh  31522  dstfrvunirn  31618  reprsuc  31772  reprpmtf1o  31783  satfvsucsuc  32496  dmopab3rexdif  32536  neifg  33603  filnetlem4  33613  ontgval  33663  bj-restsn  34254  bj-rest10  34260  bj-restpw  34264  bj-restuni  34269  mptsnunlem  34488  finxpsuclem  34547  wl-clabtv  34696  wl-clabt  34697  wl-dfrabf  34731  poimirlem16  34775  poimirlem19  34778  poimirlem23  34782  poimirlem27  34786  heicant  34794  istotbnd3  34917  sstotbnd  34921  ismtyima  34949  heibor  34967  divrngidl  35174  eccnvep  35407  ecxrn  35506  eqvrelth  35713  prtlem19  35881  prter2  35884  lkrsc  36100  lshpkr  36120  paddvaln0N  36804  paddval0  36813  diaglbN  38058  cdlemm10N  38121  lcfrvalsnN  38544  lcfrlem9  38553  lcdlss  38622  mapd1o  38651  mapd0  38668  hlhillcs  38961  fnsnbt  38985  mzpmfp  39205  lzunuz  39226  fz1eqin  39227  jm2.23  39454  pw2f1ocnv  39495  dfacbasgrp  39569  inintabd  39800  cnvcnvintabd  39821  cnvintabd  39824  rfcnpre3  41151  rfcnpre4  41152  rnmptpr  41294  iccshift  41655  iocopn  41657  iooshift  41659  iccintsng  41660  icoopn  41662  limcdm0  41760  limcresiooub  41784  limcresioolb  41785  fperdvper  42064  itgperiod  42127  fourierdlem32  42286  fourierdlem33  42287  fourierdlem48  42301  fourierdlem49  42302  fourierdlem81  42334  iccpartiun  43422  mgmhmpropd  43880  rnghmval2  43994  itsclinecirc0in  44590
  Copyright terms: Public domain W3C validator