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 1766 . 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 1870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421
This theorem is referenced by:  eqrdav  2427  eqrdavOLD  2428  uneq1  3619  ineq1  3663  unineq  3729  difin2  3741  difsn  4137  intmin4  4288  iunconst  4311  iinconst  4312  dfiun2g  4334  iindif2  4371  iinin2  4372  iunxsng  4384  opthprc  4902  inimasn  5273  dmsnopg  5327  dfco2a  5355  iotaeq  5573  imadif  5676  ssimaex  5946  unpreima  6021  respreima  6024  iinpreima  6025  fnsnb  6098  fmptsng  6100  fmptsnd  6101  tpres  6132  fconstfvOLD  6142  iunpw  6619  ordpwsuc  6656  ordsucun  6666  fun11iun  6767  reldm  6858  rntpos  6994  onoviun  7070  oarec  7271  iserd  7397  erth  7416  map0e  7517  ixpiin  7556  boxriin  7572  pw2f1olem  7682  fifo  7952  ordiso2  8030  finacn  8479  acnen  8482  acacni  8568  dfac13  8570  fin23lem26  8753  isf34lem4  8805  axdc3lem2  8879  fpwwe2lem8  9061  fpwwe2lem12  9065  fpwwe2lem13  9066  gch2  9099  gchac  9105  gchina  9123  genpass  9433  1idpr  9453  eqreznegel  11249  ixxun  11651  iccid  11681  difreicc  11762  iccsplit  11763  fzsplit2  11822  fzsn  11838  fzpr  11849  uzsplit  11864  preduz  11909  predfz  11912  fz1isolem  12619  pr2pwpr  12629  isercolllem2  13707  isercoll  13709  bitsmod  14384  bitscmp  14386  saddisj  14413  sadadd  14415  sadass  14419  smupvallem  14431  smueqlem  14438  smumul  14441  gcdcllem2  14448  vdwapun  14887  firest  15290  fncnvimaeqv  15956  mhmpropd  16539  subgacs  16803  eqgid  16820  ghmmhmb  16845  ghmpropd  16871  resscntz  16936  symg1bas  16988  lsmcom2  17242  lsmass  17255  ablnsg  17420  lsmcomx  17429  gsum2d2  17541  subgdmdprd  17602  dprd2d2  17612  unitpropd  17860  subsubrg2  17970  subrgpropd  17977  rhmpropd  17978  abvpropd  18005  lssacs  18125  lssats2  18158  lsspropd  18175  lmhmpropd  18231  lbspropd  18257  unitgOLD  19914  discld  20036  neiptopnei  20079  neiptopreu  20080  restsn  20117  restdis  20125  neitr  20127  restlp  20130  cndis  20238  cnindis  20239  cnpdis  20240  lpcls  20311  hausmapdom  20446  ptpjpre1  20517  tx1cn  20555  tx2cn  20556  hauseqlcld  20592  txkgen  20598  idqtop  20652  tgqtop  20658  acufl  20863  uffix  20867  ufildr  20877  fmfg  20895  rnelfm  20899  fmfnfm  20904  fmid  20906  fmco  20907  flimrest  20929  fclsrest  20970  alexsubALT  20997  tsmsgsum  21084  tsmssubm  21088  tsmsres  21089  tsmsf1o  21090  xpsdsval  21327  blpnf  21343  blin  21367  blres  21377  xmetec  21380  imasf1obl  21434  imasf1oxms  21435  prdsbl  21437  metrest  21470  psmetutop  21513  restmetu  21516  dscopn  21519  cnbl0  21705  bl2ioo  21721  xrtgioo  21735  cncfmet  21836  icoopnst  21863  iocopnst  21864  cldcss2  22277  iunmbl2  22387  mbfmulc2lem  22480  mbfmax  22482  ismbf3d  22487  mbfimaopnlem  22488  mbfaddlem  22493  mbfsup  22497  i1f1lem  22524  i1faddlem  22528  i1fmullem  22529  i1fmulclem  22537  i1fres  22540  mbfi1fseqlem4  22553  limcdif  22708  limcnlp  22710  limcflf  22713  limcres  22718  limcun  22727  ply1remlem  22988  fta1glem2  22992  plypf1  23034  ofmulrt  23103  plyremlem  23125  aannenlem1  23149  tglineelsb2  24536  tglinecom  24539  cusgrarn  25032  uvtxnbgra  25066  clwwlknscsh  25392  2wot2wont  25459  2spot2iun2spont  25464  nbhashuvtx  25489  vdiscusgra  25494  rusgranumwlkb0  25526  eupath2  25553  usg2spot2nb  25638  usgreg2spot  25640  numclwwlkun  25652  ubthlem1  26357  ocin  26784  shscom  26807  spansncol  27056  iunxsngf  28011  iunsnima  28064  unipreima  28085  1stpreimas  28126  1stpreima  28127  2ndpreima  28128  fpwrelmapffslem  28160  iocinioc2  28197  nndiffz1  28202  fzsplit3  28206  smatrcl  28461  fimaproj  28499  qtophaus  28502  locfinreflem  28506  prsdm  28559  prsrn  28560  indpi1  28682  indf1ofs  28686  1stmbfm  28921  2ndmbfm  28922  mbfmcnt  28929  eulerpartlemgh  29037  dstfrvunirn  29133  neifg  30812  filnetlem4  30822  ontgval  30876  mptsnunlem  31474  poimirlem16  31659  poimirlem19  31662  poimirlem23  31666  poimirlem27  31670  heicant  31678  istotbnd3  31806  sstotbnd  31810  ismtyima  31838  heibor  31856  divrngidl  31964  prtlem19  32157  prter2  32160  lkrsc  32371  lshpkr  32391  paddvaln0N  33074  paddval0  33083  diaglbN  34331  cdlemm10N  34394  lcfrvalsnN  34817  lcfrlem9  34826  lcdlss  34895  mapd1o  34924  mapd0  34941  hlhillcs  35237  mzpmfp  35297  lzunuz  35318  fz1eqin  35319  jm2.23  35556  pw2f1ocnv  35597  dfacbasgrp  35672  subrgacs  35764  sdrgacs  35765  csbabgOLD  36850  rfcnpre3  36993  rfcnpre4  36994  iunxsngf2  37043  unima  37050  iccshift  37203  iocopn  37205  iooshift  37207  iccintsng  37208  icoopn  37210  limcdm0  37269  limcresiooub  37294  limcresioolb  37295  fperdvper  37361  itgperiod  37426  fourierdlem32  37569  fourierdlem33  37570  fourierdlem48  37585  fourierdlem49  37586  fourierdlem81  37618  iccpartiun  38137  mgmhmpropd  38542  rnghmval2  38652
  Copyright terms: Public domain W3C validator