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

Theorem eqrdv 2294
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 1621 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
3 dfcleq 2290 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
42, 3sylibr 203 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530    = wceq 1632    e. wcel 1696
This theorem is referenced by:  eqrdav  2295  csbcomg  3117  csbabg  3155  uneq1  3335  ineq1  3376  unineq  3432  difin2  3443  difsn  3768  intmin4  3907  iunconst  3929  iinconst  3930  dfiun2g  3951  iindif2  3987  iinin2  3988  iunxsng  3996  iunpw  4586  ordpwsuc  4622  ordsucun  4632  opthprc  4752  dmsnopg  5160  dfco2a  5189  iotaeq  5243  imadif  5343  fun11iun  5509  ssimaex  5600  unpreima  5667  respreima  5670  iinpreima  5671  fconstfv  5750  reldm  6187  rntpos  6263  onoviun  6376  oarec  6576  iserd  6702  erth  6720  map0e  6821  ixpiin  6858  boxriin  6874  pw2f1olem  6982  fifo  7201  ordiso2  7246  finacn  7693  acnen  7696  acacni  7782  dfac13  7784  fin23lem26  7967  isf34lem4  8019  axdc3lem2  8093  fpwwe2lem8  8275  fpwwe2lem12  8279  fpwwe2lem13  8280  gchac  8311  gch2  8317  gchina  8337  genpass  8649  1idpr  8669  eqreznegel  10319  ixxun  10688  iccid  10717  difreicc  10783  iccsplit  10784  fzsplit2  10831  fzsn  10849  fzpr  10856  uzsplit  10871  fz1isolem  11415  isercolllem2  12155  isercoll  12157  bitsmod  12643  bitscmp  12645  saddisj  12672  sadadd  12674  sadass  12678  smupvallem  12690  smueqlem  12697  smumul  12700  gcdcllem2  12707  vdwapun  13037  firest  13353  mhmpropd  14437  subgacs  14668  eqgid  14685  ghmmhmb  14710  ghmpropd  14736  resscntz  14823  lsmcom2  14982  lsmass  14995  ablnsg  15155  lsmcomx  15164  gsum2d2  15241  subgdmdprd  15285  dprd2d2  15295  unitpropd  15495  subsubrg2  15588  subrgpropd  15595  rhmpropd  15596  abvpropd  15623  lssacs  15740  lssats2  15773  lsspropd  15790  lmhmpropd  15842  lbspropd  15868  unitg  16721  discld  16842  restsn  16917  restdis  16925  restlp  16929  cndis  17035  cnindis  17036  cnpdis  17037  lpcls  17108  hausmapdom  17242  ptpjpre1  17282  tx1cn  17319  tx2cn  17320  hauseqlcld  17356  txkgen  17362  idqtop  17413  tgqtop  17419  acufl  17628  uffix  17632  ufildr  17642  fmfg  17660  rnelfm  17664  fmfnfm  17669  fmid  17671  fmco  17672  flimrest  17694  fclsrest  17735  alexsubALT  17761  tsmsgsum  17837  tsmssubm  17841  tsmsres  17842  tsmsf1o  17843  xpsdsval  17961  blpnf  17970  blin  17986  blres  17993  xmetec  17996  imasf1obl  18050  imasf1oxms  18051  prdsbl  18053  metrest  18086  dscopn  18112  cnbl0  18299  bl2ioo  18314  xrtgioo  18328  cncfmet  18428  icoopnst  18453  iocopnst  18454  cldcss2  18822  iunmbl2  18930  mbfmulc2lem  19018  mbfmax  19020  ismbf3d  19025  mbfimaopnlem  19026  mbfaddlem  19031  mbfsup  19035  i1f1lem  19060  i1faddlem  19064  i1fmullem  19065  i1fmulclem  19073  i1fres  19076  mbfi1fseqlem4  19089  limcdif  19242  limcnlp  19244  limcflf  19247  limcres  19252  limcun  19261  ply1remlem  19564  fta1glem2  19568  plypf1  19610  ofmulrt  19678  plyremlem  19700  aannenlem1  19724  ubthlem1  21465  ocin  21891  shscom  21914  spansncol  22163  fzsplit3  23047  unipreima  23224  iocinioc2  23287  1stmbfm  23580  2ndmbfm  23581  mbfmcnt  23588  indpi1  23620  indf1ofs  23624  dstfrvunirn  23690  eupath2  23919  preduz  24271  predfz  24274  ontgval  24942  splint  25151  iscst4  25280  prsubrtr  25502  fgsb2  25658  iint  25715  dmrngcmp  25854  pdiveql  26271  abhp2  26278  bhp2a  26279  neifg  26423  filnetlem4  26433  istotbnd3  26598  sstotbnd  26602  ismtyima  26630  heibor  26648  divrngidl  26756  prtlem19  26849  prter2  26852  mzpmfp  26928  lzunuz  26950  fz1eqin  26951  jm2.23  27192  pw2f1ocnv  27233  dfacbasgrp  27376  subrgacs  27611  sdrgacs  27612  rfcnpre3  27807  rfcnpre4  27808  uvtxnbgra  28306  lkrsc  29909  lshpkr  29929  paddvaln0N  30612  paddval0  30621  diaglbN  31867  cdlemm10N  31930  lcfrvalsnN  32353  lcfrlem9  32362  lcdlss  32431  mapd1o  32460  mapd0  32477  hlhillcs  32773
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator