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

Theorem eqrdv 2426
Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
Hypothesis
Ref Expression
eqrdv.1  |-  ( ph  ->  ( x  e.  A  <->  x  e.  B ) )
Assertion
Ref Expression
eqrdv  |-  ( ph  ->  A  =  B )
Distinct variable groups:    x, A    x, B    ph, x

Proof of Theorem eqrdv
StepHypRef Expression
1 eqrdv.1 . . 3  |-  ( ph  ->  ( x  e.  A  <->  x  e.  B ) )
21alrimiv 1767 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
3 dfcleq 2422 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
42, 3sylibr 215 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wal 1435    = wceq 1437    e. wcel 1872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-cleq 2421
This theorem is referenced by:  eqrdav  2427  uneq1  3556  ineq1  3600  unineq  3666  difin2  3678  difsn  4077  intmin4  4228  iunconst  4251  iinconst  4252  dfiun2g  4274  iindif2  4311  iinin2  4312  iunxsng  4324  opthprc  4844  inimasn  5215  dmsnopg  5269  dfco2a  5297  iotaeq  5516  imadif  5619  ssimaex  5890  unpreima  5965  respreima  5968  iinpreima  5969  fnsnb  6042  fmptsng  6044  fmptsnd  6045  tpres  6076  fconstfvOLD  6086  iunpw  6563  ordpwsuc  6600  ordsucun  6610  fun11iun  6711  reldm  6802  rntpos  6941  onoviun  7017  oarec  7218  iserd  7344  erth  7363  map0e  7464  ixpiin  7503  boxriin  7519  pw2f1olem  7629  fifo  7899  ordiso2  7983  finacn  8432  acnen  8435  acacni  8521  dfac13  8523  fin23lem26  8706  isf34lem4  8758  axdc3lem2  8832  fpwwe2lem8  9013  fpwwe2lem12  9017  fpwwe2lem13  9018  gch2  9051  gchac  9057  gchina  9075  genpass  9385  1idpr  9405  eqreznegel  11200  ixxun  11602  iccid  11632  difreicc  11715  iccsplit  11716  fzsplit2  11775  fzsn  11791  fzpr  11802  uzsplit  11817  preduz  11862  predfz  11865  fz1isolem  12572  pr2pwpr  12584  isercolllem2  13672  isercoll  13674  bitsmod  14353  bitscmp  14355  saddisj  14382  sadadd  14384  sadass  14388  smupvallem  14400  smueqlem  14407  smumul  14410  gcdcllem2  14417  vdwapun  14867  firest  15274  fncnvimaeqv  15948  mhmpropd  16531  subgacs  16795  eqgid  16812  ghmmhmb  16837  ghmpropd  16863  resscntz  16928  symg1bas  16980  lsmcom2  17250  lsmass  17263  ablnsg  17428  lsmcomx  17437  gsum2d2  17549  subgdmdprd  17610  dprd2d2  17620  unitpropd  17868  subsubrg2  17978  subrgpropd  17985  rhmpropd  17986  abvpropd  18013  lssacs  18133  lssats2  18166  lsspropd  18183  lmhmpropd  18239  lbspropd  18265  unitgOLD  19925  discld  20047  neiptopnei  20090  neiptopreu  20091  restsn  20128  restdis  20136  neitr  20138  restlp  20141  cndis  20249  cnindis  20250  cnpdis  20251  lpcls  20322  hausmapdom  20457  ptpjpre1  20528  tx1cn  20566  tx2cn  20567  hauseqlcld  20603  txkgen  20609  idqtop  20663  tgqtop  20669  acufl  20874  uffix  20878  ufildr  20888  fmfg  20906  rnelfm  20910  fmfnfm  20915  fmid  20917  fmco  20918  flimrest  20940  fclsrest  20981  alexsubALT  21008  tsmsgsum  21095  tsmssubm  21099  tsmsres  21100  tsmsf1o  21101  xpsdsval  21338  blpnf  21354  blin  21378  blres  21388  xmetec  21391  imasf1obl  21445  imasf1oxms  21446  prdsbl  21448  metrest  21481  psmetutop  21524  restmetu  21527  dscopn  21530  cnbl0  21736  bl2ioo  21752  xrtgioo  21766  cncfmet  21882  icoopnst  21909  iocopnst  21910  cldcss2  22338  iunmbl2  22452  mbfmulc2lem  22545  mbfmax  22547  ismbf3d  22552  mbfimaopnlem  22553  mbfaddlem  22558  mbfsup  22562  i1f1lem  22589  i1faddlem  22593  i1fmullem  22594  i1fmulclem  22602  i1fres  22605  mbfi1fseqlem4  22618  limcdif  22773  limcnlp  22775  limcflf  22778  limcres  22783  limcun  22792  ply1remlem  23055  fta1glem2  23059  plypf1  23108  ofmulrt  23177  plyremlem  23199  aannenlem1  23226  tglineelsb2  24619  tglinecom  24622  cusgrarn  25129  uvtxnbgra  25163  clwwlknscsh  25489  2wot2wont  25556  2spot2iun2spont  25561  nbhashuvtx  25586  vdiscusgra  25591  rusgranumwlkb0  25623  eupath2  25650  usg2spot2nb  25735  usgreg2spot  25737  numclwwlkun  25749  ubthlem1  26454  ocin  26891  shscom  26914  spansncol  27163  iunxsngf  28118  iunsnima  28170  unipreima  28191  1stpreimas  28232  1stpreima  28233  2ndpreima  28234  fpwrelmapffslem  28267  iocinioc2  28311  nndiffz1  28316  fzsplit3  28320  smatrcl  28574  fimaproj  28612  qtophaus  28615  locfinreflem  28619  prsdm  28672  prsrn  28673  indpi1  28795  indf1ofs  28799  1stmbfm  29034  2ndmbfm  29035  mbfmcnt  29042  eulerpartlemgh  29163  dstfrvunirn  29259  neifg  30976  filnetlem4  30986  ontgval  31040  mptsnunlem  31647  finxpsuclem  31696  poimirlem16  31863  poimirlem19  31866  poimirlem23  31870  poimirlem27  31874  heicant  31882  istotbnd3  32010  sstotbnd  32014  ismtyima  32042  heibor  32060  divrngidl  32168  prtlem19  32361  prter2  32364  lkrsc  32575  lshpkr  32595  paddvaln0N  33278  paddval0  33287  diaglbN  34535  cdlemm10N  34598  lcfrvalsnN  35021  lcfrlem9  35030  lcdlss  35099  mapd1o  35128  mapd0  35145  hlhillcs  35441  mzpmfp  35501  lzunuz  35522  fz1eqin  35523  jm2.23  35764  pw2f1ocnv  35805  dfacbasgrp  35880  subrgacs  35979  sdrgacs  35980  inintabd  36098  cnvcnvintabd  36119  cnvintabd  36122  csbabgOLD  37127  rfcnpre3  37270  rfcnpre4  37271  iunxsngf2  37318  unima  37332  iccshift  37511  iocopn  37513  iooshift  37515  iccintsng  37516  icoopn  37518  limcdm0  37581  limcresiooub  37606  limcresioolb  37607  fperdvper  37673  itgperiod  37741  fourierdlem32  37885  fourierdlem33  37886  fourierdlem48  37901  fourierdlem49  37902  fourierdlem81  37934  iccpartiun  38561  usgredgedga  39064  nbumgrvtx  39160  mgmhmpropd  39386  rnghmval2  39496
  Copyright terms: Public domain W3C validator