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

Theorem eqrdv 2439
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 2435 . 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 1362    = wceq 1364    e. wcel 1761
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 2422
This theorem depends on definitions:  df-bi 185  df-cleq 2434
This theorem is referenced by:  eqrdav  2440  uneq1  3500  ineq1  3542  unineq  3597  difin2  3609  csbcomgOLD  3687  csbabgOLD  3705  difsn  4005  intmin4  4154  iunconst  4176  iinconst  4177  dfiun2g  4199  iindif2  4236  iinin2  4237  iunxsng  4246  opthprc  4882  inimasn  5251  dmsnopg  5307  dfco2a  5335  iotaeq  5386  imadif  5490  ssimaex  5753  unpreima  5826  respreima  5829  iinpreima  5830  fmptsng  5897  fconstfv  5937  iunpw  6389  ordpwsuc  6425  ordsucun  6435  fun11iun  6536  reldm  6624  rntpos  6757  onoviun  6800  oarec  6997  iserd  7123  erth  7141  map0e  7246  ixpiin  7285  boxriin  7301  pw2f1olem  7411  fifo  7678  ordiso2  7725  finacn  8216  acnen  8219  acacni  8305  dfac13  8307  fin23lem26  8490  isf34lem4  8542  axdc3lem2  8616  fpwwe2lem8  8800  fpwwe2lem12  8804  fpwwe2lem13  8805  gch2  8838  gchac  8844  gchina  8862  genpass  9174  1idpr  9194  eqreznegel  10936  ixxun  11312  iccid  11341  difreicc  11413  iccsplit  11414  fzsplit2  11470  fzsn  11496  fzpr  11507  uzsplit  11526  pr2pwpr  12179  fz1isolem  12210  isercolllem2  13139  isercoll  13141  bitsmod  13628  bitscmp  13630  saddisj  13657  sadadd  13659  sadass  13663  smupvallem  13675  smueqlem  13682  smumul  13685  gcdcllem2  13692  vdwapun  14031  firest  14367  mhmpropd  15466  subgacs  15709  eqgid  15726  ghmmhmb  15751  ghmpropd  15777  resscntz  15842  symg1bas  15894  lsmcom2  16147  lsmass  16160  ablnsg  16322  lsmcomx  16331  gsum2d2  16456  subgdmdprd  16521  dprd2d2  16533  unitpropd  16779  subsubrg2  16872  subrgpropd  16879  rhmpropd  16880  abvpropd  16907  lssacs  17026  lssats2  17059  lsspropd  17076  lmhmpropd  17132  lbspropd  17158  unitg  18531  discld  18652  neiptopnei  18695  neiptopreu  18696  restsn  18733  restdis  18741  neitr  18743  restlp  18746  cndis  18854  cnindis  18855  cnpdis  18856  lpcls  18927  hausmapdom  19063  ptpjpre1  19103  tx1cn  19141  tx2cn  19142  hauseqlcld  19178  txkgen  19184  idqtop  19238  tgqtop  19244  acufl  19449  uffix  19453  ufildr  19463  fmfg  19481  rnelfm  19485  fmfnfm  19490  fmid  19492  fmco  19493  flimrest  19515  fclsrest  19556  alexsubALT  19582  tsmsgsum  19668  tsmsgsumOLD  19671  tsmssubm  19675  tsmsresOLD  19676  tsmsres  19677  tsmsf1o  19678  xpsdsval  19915  blpnf  19931  blin  19955  blres  19965  xmetec  19968  imasf1obl  20022  imasf1oxms  20023  prdsbl  20025  metrest  20058  metutopOLD  20116  psmetutop  20117  restmetu  20121  dscopn  20125  cnbl0  20312  bl2ioo  20328  xrtgioo  20342  cncfmet  20443  icoopnst  20470  iocopnst  20471  cldcss2  20888  iunmbl2  20997  mbfmulc2lem  21084  mbfmax  21086  ismbf3d  21091  mbfimaopnlem  21092  mbfaddlem  21097  mbfsup  21101  i1f1lem  21126  i1faddlem  21130  i1fmullem  21131  i1fmulclem  21139  i1fres  21142  mbfi1fseqlem4  21155  limcdif  21310  limcnlp  21312  limcflf  21315  limcres  21320  limcun  21329  ply1remlem  21593  fta1glem2  21597  plypf1  21639  ofmulrt  21707  plyremlem  21729  aannenlem1  21753  tglineelsb2  22992  tglinecom  22995  cusgrarn  23302  uvtxnbgra  23336  eupath2  23536  ubthlem1  24206  ocin  24634  shscom  24657  spansncol  24906  unipreima  25896  1stpreima  25936  2ndpreima  25937  fpwrelmapffslem  25967  iocinioc2  26002  nndiffz1  26008  fzsplit3  26011  prsdm  26280  prsrn  26281  indpi1  26414  indf1ofs  26418  1stmbfm  26611  2ndmbfm  26612  mbfmcnt  26619  eulerpartlemgh  26691  dstfrvunirn  26787  preduz  27590  predfz  27593  ontgval  28207  heicant  28351  neifg  28517  filnetlem4  28527  istotbnd3  28595  sstotbnd  28599  ismtyima  28627  heibor  28645  divrngidl  28753  iuneq2f  28892  prtlem19  28948  prter2  28951  mzpmfp  29008  mzpmfpOLD  29009  lzunuz  29031  fz1eqin  29032  jm2.23  29270  pw2f1ocnv  29311  dfacbasgrp  29389  subrgacs  29482  sdrgacs  29483  rfcnpre3  29680  rfcnpre4  29681  2wot2wont  30330  2spot2iun2spont  30335  Lemma2  30418  nbhashuvtx  30459  vdiscusgra  30462  rusgranumwlkb0  30496  usg2spot2nb  30583  usgreg2spot  30585  numclwwlkun  30597  fmptsnd  30646  lkrsc  32464  lshpkr  32484  paddvaln0N  33167  paddval0  33176  diaglbN  34422  cdlemm10N  34485  lcfrvalsnN  34908  lcfrlem9  34917  lcdlss  34986  mapd1o  35015  mapd0  35032  hlhillcs  35328
  Copyright terms: Public domain W3C validator