Theorem eqrdv 2620

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

Step	Hyp	Ref	Expression
1		eqrdv.1	. . 3 |- ( ph -> ( x e. A <-> x e. B ) )
2	1	alrimiv 1855	. 2 |- ( ph -> A. x ( x e. A <-> x e. B ) )
3		dfcleq 2616	. 2 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
4	2, 3	sylibr 224	1 |- ( ph -> A = B )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  eqrdav  2621  uneq1  3760  ineq1  3807  unineq  3877  difin2  3890  difsn  4328  intmin4  4506  iunconst  4529  iinconst  4530  dfiun2g  4552  iindif2  4589  iinin2  4590  iunxsng  4602  opthprc  5167  inimasn  5550  dmsnopg  5606  dfco2a  5635  iotaeq  5859  imadif  5973  ssimaex  6263  unpreima  6341  respreima  6344  iinpreima  6345  fnsnb  6432  fmptsng  6434  fmptsnd  6435  tpres  6466  iunpw  6978  ordpwsuc  7015  ordsucun  7025  fun11iun  7126  reldm  7219  rntpos  7365  onoviun  7440  oarec  7642  iserd  7768  erth  7791  mapdm0  7872  map0e  7895  ixpiin  7934  boxriin  7950  pw2f1olem  8064  fifo  8338  ordiso2  8420  finacn  8873  acnen  8876  acacni  8962  dfac13  8964  fin23lem26  9147  isf34lem4  9199  axdc3lem2  9273  fpwwe2lem8  9459  fpwwe2lem12  9463  fpwwe2lem13  9464  gch2  9497  gchac  9503  gchina  9521  genpass  9831  1idpr  9851  eqreznegel  11774  ixxun  12191  iccid  12220  difreicc  12304  iccsplit  12305  fzsplit2  12366  fzsn  12383  fzpr  12396  uzsplit  12412  preduz  12461  predfz  12464  fz1isolem  13245  pr2pwpr  13261  isercolllem2  14396  isercoll  14398  bitsmod  15158  bitscmp  15160  saddisj  15187  sadadd  15189  sadass  15193  smupvallem  15205  smueqlem  15212  smumul  15215  gcdcllem2  15222  vdwapun  15678  firest  16093  fncnvimaeqv  16760  mhmpropd  17341  subgacs  17629  eqgid  17646  ghmmhmb  17671  ghmpropd  17698  resscntz  17764  symg1bas  17816  lsmcom2  18070  lsmass  18083  ablnsg  18250  lsmcomx  18259  gsum2d2  18373  subgdmdprd  18433  dprd2d2  18443  unitpropd  18697  subsubrg2  18807  subrgpropd  18814  rhmpropd  18815  abvpropd  18842  lssacs  18967  lssats2  19000  lsspropd  19017  lmhmpropd  19073  lbspropd  19099  discld  20893  neiptopnei  20936  neiptopreu  20937  restsn  20974  restdis  20982  neitr  20984  restlp  20987  cndis  21095  cnindis  21096  cnpdis  21097  lpcls  21168  hausmapdom  21303  ptpjpre1  21374  tx1cn  21412  tx2cn  21413  hauseqlcld  21449  txkgen  21455  idqtop  21509  tgqtop  21515  acufl  21721  uffix  21725  ufildr  21735  fmfg  21753  rnelfm  21757  fmfnfm  21762  fmid  21764  fmco  21765  flimrest  21787  fclsrest  21828  alexsubALT  21855  tsmsgsum  21942  tsmssubm  21946  tsmsres  21947  tsmsf1o  21948  xpsdsval  22186  blpnf  22202  blin  22226  blres  22236  xmetec  22239  imasf1obl  22293  imasf1oxms  22294  prdsbl  22296  metrest  22329  psmetutop  22372  restmetu  22375  dscopn  22378  cnbl0  22577  bl2ioo  22595  xrtgioo  22609  cncfmet  22711  icoopnst  22738  iocopnst  22739  cldcss2  23213  iunmbl2  23325  mbfmulc2lem  23414  mbfmax  23416  ismbf3d  23421  mbfimaopnlem  23422  mbfaddlem  23427  mbfsup  23431  i1f1lem  23456  i1faddlem  23460  i1fmullem  23461  i1fmulclem  23469  i1fres  23472  mbfi1fseqlem4  23485  limcdif  23640  limcnlp  23642  limcflf  23645  limcres  23650  limcun  23659  ply1remlem  23922  fta1glem2  23926  plypf1  23968  ofmulrt  24037  plyremlem  24059  aannenlem1  24083  gausslemma2dlem1a  25090  tglineelsb2  25527  tglinecom  25530  ushgredgedg  26121  ushgredgedgloop  26123  nbumgrvtx  26242  nbusgrvtxm1uvtx  26306  vdiscusgr  26427  wspniunwspnon  26819  rusgrnumwwlkb0  26866  clwwlksnscsh  26940  clwwlksnun  26974  eupth2lems  27098  fusgr2wsp2nb  27198  fusgreg2wsp  27200  ubthlem1  27726  ocin  28155  shscom  28178  spansncol  28427  iunxsngf  29375  iunsnima  29428  unipreima  29446  1stpreimas  29483  1stpreima  29484  2ndpreima  29485  fpwrelmapffslem  29507  iocinioc2  29541  nndiffz1  29548  fzsplit3  29553  smatrcl  29862  fimaproj  29900  qtophaus  29903  locfinreflem  29907  prsdm  29960  prsrn  29961  indpi1  30082  indf1ofs  30088  1stmbfm  30322  2ndmbfm  30323  mbfmcnt  30330  eulerpartlemgh  30440  dstfrvunirn  30536  reprsuc  30693  reprpmtf1o  30704  neifg  32366  filnetlem4  32376  ontgval  32430  bj-restsn  33035  bj-rest10  33041  bj-restpw  33045  bj-restuni  33050  mptsnunlem  33185  finxpsuclem  33234  poimirlem16  33425  poimirlem19  33428  poimirlem23  33432  poimirlem27  33436  heicant  33444  istotbnd3  33570  sstotbnd  33574  ismtyima  33602  heibor  33620  divrngidl  33827  eccnvep  34047  prtlem19  34163  prter2  34166  lkrsc  34384  lshpkr  34404  paddvaln0N  35087  paddval0  35096  diaglbN  36344  cdlemm10N  36407  lcfrvalsnN  36830  lcfrlem9  36839  lcdlss  36908  mapd1o  36937  mapd0  36954  hlhillcs  37250  mzpmfp  37310  lzunuz  37331  fz1eqin  37332  jm2.23  37563  pw2f1ocnv  37604  dfacbasgrp  37678  subrgacs  37770  sdrgacs  37771  inintabd  37885  cnvcnvintabd  37906  cnvintabd  37909  csbabgOLD  39050  rfcnpre3  39192  rfcnpre4  39193  iunxsngf2  39230  unima  39346  iccshift  39744  iocopn  39746  iooshift  39748  iccintsng  39749  icoopn  39751  limcdm0  39850  limcresiooub  39874  limcresioolb  39875  fperdvper  40133  itgperiod  40197  fourierdlem32  40356  fourierdlem33  40357  fourierdlem48  40371  fourierdlem49  40372  fourierdlem81  40404  iccpartiun  41370  mgmhmpropd  41785  rnghmval2  41895