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

Theorem eqrdv 2649
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 1895 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfcleq 2645 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 224 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521   = wceq 1523  wcel 2030
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-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  eqrdav  2650  uneq1  3793  ineq1  3840  unineq  3910  difin2  3923  difsn  4360  intmin4  4538  iunconst  4561  iinconst  4562  dfiun2g  4584  iindif2  4621  iinin2  4622  iunxsng  4634  opthprc  5201  inimasn  5585  dmsnopg  5642  dfco2a  5673  iotaeq  5897  imadif  6011  ssimaex  6302  unpreima  6381  respreima  6384  iinpreima  6385  fnsnb  6473  fmptsng  6475  fmptsnd  6476  tpres  6507  iunpw  7020  ordpwsuc  7057  ordsucun  7067  fun11iun  7168  reldm  7263  rntpos  7410  onoviun  7485  oarec  7687  iserd  7813  erth  7834  mapdm0  7914  map0e  7937  ixpiin  7976  boxriin  7992  pw2f1olem  8105  fifo  8379  ordiso2  8461  finacn  8911  acnen  8914  acacni  9000  dfac13  9002  fin23lem26  9185  isf34lem4  9237  axdc3lem2  9311  fpwwe2lem8  9497  fpwwe2lem12  9501  fpwwe2lem13  9502  gch2  9535  gchac  9541  gchina  9559  genpass  9869  1idpr  9889  eqreznegel  11812  ixxun  12229  iccid  12258  difreicc  12342  iccsplit  12343  fzsplit2  12404  fzsn  12421  fzpr  12434  uzsplit  12450  preduz  12500  predfz  12503  fz1isolem  13283  pr2pwpr  13299  isercolllem2  14440  isercoll  14442  bitsmod  15205  bitscmp  15207  saddisj  15234  sadadd  15236  sadass  15240  smupvallem  15252  smueqlem  15259  smumul  15262  gcdcllem2  15269  vdwapun  15725  firest  16140  fncnvimaeqv  16807  mhmpropd  17388  subgacs  17676  eqgid  17693  ghmmhmb  17718  ghmpropd  17745  resscntz  17810  symg1bas  17862  lsmcom2  18116  lsmass  18129  ablnsg  18296  lsmcomx  18305  gsum2d2  18419  subgdmdprd  18479  dprd2d2  18489  unitpropd  18743  subsubrg2  18855  subrgpropd  18862  rhmpropd  18863  abvpropd  18890  lssacs  19015  lssats2  19048  lsspropd  19065  lmhmpropd  19121  lbspropd  19147  discld  20941  neiptopnei  20984  neiptopreu  20985  restsn  21022  restdis  21030  neitr  21032  restlp  21035  cndis  21143  cnindis  21144  cnpdis  21145  lpcls  21216  hausmapdom  21351  ptpjpre1  21422  tx1cn  21460  tx2cn  21461  hauseqlcld  21497  txkgen  21503  idqtop  21557  tgqtop  21563  acufl  21768  uffix  21772  ufildr  21782  fmfg  21800  rnelfm  21804  fmfnfm  21809  fmid  21811  fmco  21812  flimrest  21834  fclsrest  21875  alexsubALT  21902  tsmsgsum  21989  tsmssubm  21993  tsmsres  21994  tsmsf1o  21995  xpsdsval  22233  blpnf  22249  blin  22273  blres  22283  xmetec  22286  imasf1obl  22340  imasf1oxms  22341  prdsbl  22343  metrest  22376  psmetutop  22419  restmetu  22422  dscopn  22425  cnbl0  22624  bl2ioo  22642  xrtgioo  22656  cncfmet  22758  icoopnst  22785  iocopnst  22786  cldcss2  23259  iunmbl2  23371  mbfmulc2lem  23459  mbfmax  23461  ismbf3d  23466  mbfimaopnlem  23467  mbfaddlem  23472  mbfsup  23476  i1f1lem  23501  i1faddlem  23505  i1fmullem  23506  i1fmulclem  23514  i1fres  23517  mbfi1fseqlem4  23530  limcdif  23685  limcnlp  23687  limcflf  23690  limcres  23695  limcun  23704  ply1remlem  23967  fta1glem2  23971  plypf1  24013  ofmulrt  24082  plyremlem  24104  aannenlem1  24128  gausslemma2dlem1a  25135  tglineelsb2  25572  tglinecom  25575  ushgredgedg  26166  ushgredgedgloop  26168  nbumgrvtx  26287  nbusgrvtxm1uvtx  26356  vdiscusgr  26483  wspniunwspnon  26888  rusgrnumwwlkb0  26938  clwwlknscsh  27027  clwwlknun  27087  clwwlknunOLD  27091  eupth2lems  27216  fusgr2wsp2nb  27314  fusgreg2wsp  27316  ubthlem1  27854  ocin  28283  shscom  28306  spansncol  28555  iunxsngf  29501  iunsnima  29556  unipreima  29574  1stpreimas  29611  1stpreima  29612  2ndpreima  29613  fpwrelmapffslem  29635  iocinioc2  29669  nndiffz1  29676  fzsplit3  29681  smatrcl  29990  fimaproj  30028  qtophaus  30031  locfinreflem  30035  prsdm  30088  prsrn  30089  indpi1  30210  indf1ofs  30216  1stmbfm  30450  2ndmbfm  30451  mbfmcnt  30458  eulerpartlemgh  30568  dstfrvunirn  30664  reprsuc  30821  reprpmtf1o  30832  neifg  32491  filnetlem4  32501  ontgval  32555  bj-restsn  33160  bj-rest10  33166  bj-restpw  33170  bj-restuni  33175  mptsnunlem  33315  finxpsuclem  33364  poimirlem16  33555  poimirlem19  33558  poimirlem23  33562  poimirlem27  33566  heicant  33574  istotbnd3  33700  sstotbnd  33704  ismtyima  33732  heibor  33750  divrngidl  33957  eccnvep  34188  ecxrn  34289  prtlem19  34482  prter2  34485  lkrsc  34702  lshpkr  34722  paddvaln0N  35405  paddval0  35414  diaglbN  36661  cdlemm10N  36724  lcfrvalsnN  37147  lcfrlem9  37156  lcdlss  37225  mapd1o  37254  mapd0  37271  hlhillcs  37567  mzpmfp  37627  lzunuz  37648  fz1eqin  37649  jm2.23  37880  pw2f1ocnv  37921  dfacbasgrp  37995  subrgacs  38087  sdrgacs  38088  inintabd  38202  cnvcnvintabd  38223  cnvintabd  38226  csbabgOLD  39367  rfcnpre3  39506  rfcnpre4  39507  iunxsngf2  39544  unima  39660  iccshift  40062  iocopn  40064  iooshift  40066  iccintsng  40067  icoopn  40069  limcdm0  40168  limcresiooub  40192  limcresioolb  40193  fperdvper  40451  itgperiod  40515  fourierdlem32  40674  fourierdlem33  40675  fourierdlem48  40689  fourierdlem49  40690  fourierdlem81  40722  iccpartiun  41695  mgmhmpropd  42110  rnghmval2  42220
  Copyright terms: Public domain W3C validator