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

Theorem eqrdv 2441
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 1685 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
3 dfcleq 2437 . 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 1367    = wceq 1369    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-cleq 2436
This theorem is referenced by:  eqrdav  2442  uneq1  3506  ineq1  3548  unineq  3603  difin2  3615  csbcomgOLD  3693  csbabgOLD  3711  difsn  4011  intmin4  4160  iunconst  4182  iinconst  4183  dfiun2g  4205  iindif2  4242  iinin2  4243  iunxsng  4252  opthprc  4889  inimasn  5257  dmsnopg  5313  dfco2a  5341  iotaeq  5392  imadif  5496  ssimaex  5759  unpreima  5832  respreima  5835  iinpreima  5836  fmptsng  5903  fconstfv  5943  iunpw  6393  ordpwsuc  6429  ordsucun  6439  fun11iun  6540  reldm  6628  rntpos  6761  onoviun  6807  oarec  7004  iserd  7130  erth  7148  map0e  7253  ixpiin  7292  boxriin  7308  pw2f1olem  7418  fifo  7685  ordiso2  7732  finacn  8223  acnen  8226  acacni  8312  dfac13  8314  fin23lem26  8497  isf34lem4  8549  axdc3lem2  8623  fpwwe2lem8  8807  fpwwe2lem12  8811  fpwwe2lem13  8812  gch2  8845  gchac  8851  gchina  8869  genpass  9181  1idpr  9201  eqreznegel  10943  ixxun  11319  iccid  11348  difreicc  11420  iccsplit  11421  fzsplit2  11477  fzsn  11503  fzpr  11514  uzsplit  11533  pr2pwpr  12186  fz1isolem  12217  isercolllem2  13146  isercoll  13148  bitsmod  13635  bitscmp  13637  saddisj  13664  sadadd  13666  sadass  13670  smupvallem  13682  smueqlem  13689  smumul  13692  gcdcllem2  13699  vdwapun  14038  firest  14374  mhmpropd  15473  subgacs  15719  eqgid  15736  ghmmhmb  15761  ghmpropd  15787  resscntz  15852  symg1bas  15904  lsmcom2  16157  lsmass  16170  ablnsg  16332  lsmcomx  16341  gsum2d2  16469  subgdmdprd  16534  dprd2d2  16546  unitpropd  16792  subsubrg2  16895  subrgpropd  16902  rhmpropd  16903  abvpropd  16930  lssacs  17051  lssats2  17084  lsspropd  17101  lmhmpropd  17157  lbspropd  17183  unitg  18575  discld  18696  neiptopnei  18739  neiptopreu  18740  restsn  18777  restdis  18785  neitr  18787  restlp  18790  cndis  18898  cnindis  18899  cnpdis  18900  lpcls  18971  hausmapdom  19107  ptpjpre1  19147  tx1cn  19185  tx2cn  19186  hauseqlcld  19222  txkgen  19228  idqtop  19282  tgqtop  19288  acufl  19493  uffix  19497  ufildr  19507  fmfg  19525  rnelfm  19529  fmfnfm  19534  fmid  19536  fmco  19537  flimrest  19559  fclsrest  19600  alexsubALT  19626  tsmsgsum  19712  tsmsgsumOLD  19715  tsmssubm  19719  tsmsresOLD  19720  tsmsres  19721  tsmsf1o  19722  xpsdsval  19959  blpnf  19975  blin  19999  blres  20009  xmetec  20012  imasf1obl  20066  imasf1oxms  20067  prdsbl  20069  metrest  20102  metutopOLD  20160  psmetutop  20161  restmetu  20165  dscopn  20169  cnbl0  20356  bl2ioo  20372  xrtgioo  20386  cncfmet  20487  icoopnst  20514  iocopnst  20515  cldcss2  20932  iunmbl2  21041  mbfmulc2lem  21128  mbfmax  21130  ismbf3d  21135  mbfimaopnlem  21136  mbfaddlem  21141  mbfsup  21145  i1f1lem  21170  i1faddlem  21174  i1fmullem  21175  i1fmulclem  21183  i1fres  21186  mbfi1fseqlem4  21199  limcdif  21354  limcnlp  21356  limcflf  21359  limcres  21364  limcun  21373  ply1remlem  21637  fta1glem2  21641  plypf1  21683  ofmulrt  21751  plyremlem  21773  aannenlem1  21797  tglineelsb2  23041  tglinecom  23044  cusgrarn  23370  uvtxnbgra  23404  eupath2  23604  ubthlem1  24274  ocin  24702  shscom  24725  spansncol  24974  unipreima  25964  1stpreima  26004  2ndpreima  26005  fpwrelmapffslem  26035  iocinioc2  26072  nndiffz1  26078  fzsplit3  26081  prsdm  26347  prsrn  26348  indpi1  26481  indf1ofs  26485  1stmbfm  26678  2ndmbfm  26679  mbfmcnt  26686  eulerpartlemgh  26764  dstfrvunirn  26860  preduz  27664  predfz  27667  ontgval  28280  heicant  28429  neifg  28595  filnetlem4  28605  istotbnd3  28673  sstotbnd  28677  ismtyima  28705  heibor  28723  divrngidl  28831  iuneq2f  28970  prtlem19  29026  prter2  29029  mzpmfp  29086  mzpmfpOLD  29087  lzunuz  29109  fz1eqin  29110  jm2.23  29348  pw2f1ocnv  29389  dfacbasgrp  29467  subrgacs  29560  sdrgacs  29561  rfcnpre3  29758  rfcnpre4  29759  2wot2wont  30408  2spot2iun2spont  30413  Lemma2  30496  nbhashuvtx  30537  vdiscusgra  30540  rusgranumwlkb0  30574  usg2spot2nb  30661  usgreg2spot  30663  numclwwlkun  30675  fmptsnd  30725  lkrsc  32745  lshpkr  32765  paddvaln0N  33448  paddval0  33457  diaglbN  34703  cdlemm10N  34766  lcfrvalsnN  35189  lcfrlem9  35198  lcdlss  35267  mapd1o  35296  mapd0  35313  hlhillcs  35609
  Copyright terms: Public domain W3C validator