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

Theorem eqrdv 2457
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 1690 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
3 dfcleq 2453 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
42, 3sylibr 212 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1372    = wceq 1374    e. wcel 1762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-cleq 2452
This theorem is referenced by:  eqrdav  2458  eqrdavOLD  2459  uneq1  3644  ineq1  3686  unineq  3741  difin2  3753  csbcomgOLD  3831  csbabgOLD  3849  difsn  4154  intmin4  4304  iunconst  4327  iinconst  4328  dfiun2g  4350  iindif2  4387  iinin2  4388  iunxsng  4397  opthprc  5039  inimasn  5414  dmsnopg  5470  dfco2a  5498  iotaeq  5550  imadif  5654  ssimaex  5923  unpreima  5998  respreima  6001  iinpreima  6002  fmptsng  6073  fmptsnd  6074  fconstfv  6114  iunpw  6585  ordpwsuc  6621  ordsucun  6631  fun11iun  6734  reldm  6825  rntpos  6958  onoviun  7004  oarec  7201  iserd  7327  erth  7346  map0e  7446  ixpiin  7485  boxriin  7501  pw2f1olem  7611  fifo  7881  ordiso2  7929  finacn  8420  acnen  8423  acacni  8509  dfac13  8511  fin23lem26  8694  isf34lem4  8746  axdc3lem2  8820  fpwwe2lem8  9004  fpwwe2lem12  9008  fpwwe2lem13  9009  gch2  9042  gchac  9048  gchina  9066  genpass  9376  1idpr  9396  eqreznegel  11156  ixxun  11534  iccid  11563  difreicc  11641  iccsplit  11642  fzsplit2  11699  fzsn  11714  fzpr  11724  uzsplit  11739  fz1isolem  12463  pr2pwpr  12473  isercolllem2  13437  isercoll  13439  bitsmod  13934  bitscmp  13936  saddisj  13963  sadadd  13965  sadass  13969  smupvallem  13981  smueqlem  13988  smumul  13991  gcdcllem2  13998  vdwapun  14340  firest  14677  mhmpropd  15776  subgacs  16024  eqgid  16041  ghmmhmb  16066  ghmpropd  16092  resscntz  16157  symg1bas  16209  lsmcom2  16464  lsmass  16477  ablnsg  16639  lsmcomx  16648  gsum2d2  16786  subgdmdprd  16864  dprd2d2  16876  unitpropd  17123  subsubrg2  17232  subrgpropd  17239  rhmpropd  17240  abvpropd  17267  lssacs  17389  lssats2  17422  lsspropd  17439  lmhmpropd  17495  lbspropd  17521  unitg  19228  discld  19349  neiptopnei  19392  neiptopreu  19393  restsn  19430  restdis  19438  neitr  19440  restlp  19443  cndis  19551  cnindis  19552  cnpdis  19553  lpcls  19624  hausmapdom  19760  ptpjpre1  19800  tx1cn  19838  tx2cn  19839  hauseqlcld  19875  txkgen  19881  idqtop  19935  tgqtop  19941  acufl  20146  uffix  20150  ufildr  20160  fmfg  20178  rnelfm  20182  fmfnfm  20187  fmid  20189  fmco  20190  flimrest  20212  fclsrest  20253  alexsubALT  20279  tsmsgsum  20365  tsmsgsumOLD  20368  tsmssubm  20372  tsmsresOLD  20373  tsmsres  20374  tsmsf1o  20375  xpsdsval  20612  blpnf  20628  blin  20652  blres  20662  xmetec  20665  imasf1obl  20719  imasf1oxms  20720  prdsbl  20722  metrest  20755  metutopOLD  20813  psmetutop  20814  restmetu  20818  dscopn  20822  cnbl0  21009  bl2ioo  21025  xrtgioo  21039  cncfmet  21140  icoopnst  21167  iocopnst  21168  cldcss2  21585  iunmbl2  21695  mbfmulc2lem  21782  mbfmax  21784  ismbf3d  21789  mbfimaopnlem  21790  mbfaddlem  21795  mbfsup  21799  i1f1lem  21824  i1faddlem  21828  i1fmullem  21829  i1fmulclem  21837  i1fres  21840  mbfi1fseqlem4  21853  limcdif  22008  limcnlp  22010  limcflf  22013  limcres  22018  limcun  22027  ply1remlem  22291  fta1glem2  22295  plypf1  22337  ofmulrt  22405  plyremlem  22427  aannenlem1  22451  tglineelsb2  23719  tglinecom  23722  cusgrarn  24121  uvtxnbgra  24155  clwwlknscsh  24481  2wot2wont  24548  2spot2iun2spont  24553  nbhashuvtx  24578  vdiscusgra  24583  rusgranumwlkb0  24615  eupath2  24642  usg2spot2nb  24728  usgreg2spot  24730  numclwwlkun  24742  ubthlem1  25448  ocin  25876  shscom  25899  spansncol  26148  unipreima  27142  1stpreima  27182  2ndpreima  27183  fpwrelmapffslem  27213  iocinioc2  27244  nndiffz1  27250  fzsplit3  27253  fimaproj  27485  prsdm  27518  prsrn  27519  qtophaus  27623  indpi1  27661  indf1ofs  27665  1stmbfm  27857  2ndmbfm  27858  mbfmcnt  27865  eulerpartlemgh  27943  dstfrvunirn  28039  preduz  28843  predfz  28846  ontgval  29459  heicant  29613  neifg  29779  filnetlem4  29789  istotbnd3  29857  sstotbnd  29861  ismtyima  29889  heibor  29907  divrngidl  30015  iuneq2f  30154  prtlem19  30210  prter2  30213  mzpmfp  30270  mzpmfpOLD  30271  lzunuz  30292  fz1eqin  30293  jm2.23  30531  pw2f1ocnv  30572  dfacbasgrp  30650  subrgacs  30743  sdrgacs  30744  rfcnpre3  30941  rfcnpre4  30942  unima  30974  iccintsng  31082  lkrsc  33769  lshpkr  33789  paddvaln0N  34472  paddval0  34481  diaglbN  35727  cdlemm10N  35790  lcfrvalsnN  36213  lcfrlem9  36222  lcdlss  36291  mapd1o  36320  mapd0  36337  hlhillcs  36633
  Copyright terms: Public domain W3C validator