Theorem eqrdv 2767

Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)

Hypothesis

Ref	Expression
eqrdv.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Assertion

Ref	Expression
eqrdv	⊢ (𝜑 → 𝐴 = 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Proof of Theorem eqrdv

Step	Hyp	Ref	Expression
1		eqrdv.1	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	alrimiv 1954	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfcleq 2762	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	2, 3	sylibr 237	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  eqrdav  2768  abbi  2834  eqabdv  2902  uneq1  4123  unineq  4249  difin2  4262  difsn  4770  intmin4  4946  intprg  4950  iunconst  4970  iinconst  4971  iuneqconst  4972  dfiun2g  4998  iindif1  5045  iindif2  5047  iinin2  5048  iunxsng  5060  iunxsngf  5062  opthprc  5726  dmopab2rex  5908  dmxp  5920  epin  6098  inimasn  6154  dmsnopg  6215  dfco2a  6248  iotaeq  6505  imadif  6621  unima  6957  ssimaex  6967  unpreima  7059  respreima  7062  iinpreima  7065  fnsnbg  7163  fnsnbOLD  7165  fmptsng  7167  fmptsnd  7168  tpres  7200  iunpw  7769  ordpwsuc  7810  ordsucun  7820  fiun  7939  f1iun  7940  reldm  8040  fimaproj  8130  xpord2pred  8140  xpord3pred  8147  rntpos  8234  onoviun  8329  oarec  8546  iserd  8720  erth  8748  mapdm0  8838  mapfset  8846  ixpiin  8921  boxriin  8937  pw2f1olem  9068  fifo  9391  ordiso2  9476  ttrclse  9695  finacn  10033  acnen  10036  acacni  10123  dfac13  10125  fin23lem26  10308  isf34lem4  10360  axdc3lem2  10434  fpwwe2lem7  10621  fpwwe2lem11  10625  fpwwe2lem12  10626  gch2  10659  gchac  10665  gchina  10683  genpass  10993  1idpr  11013  indpi1  12231  eqreznegel  12957  ixxun  13387  iccid  13416  difreicc  13510  iccsplit  13511  fzsplit2  13576  fzsn  13593  fzpr  13606  uzsplit  13623  fzdif1  13632  preduz  13677  predfz  13680  fz1isolem  14497  pr2pwpr  14515  isercolllem2  15716  isercoll  15718  bitsmod  16493  bitscmp  16495  saddisj  16522  sadadd  16524  sadass  16528  smupvallem  16540  smueqlem  16547  smumul  16550  gcdcllem2  16557  vdwapun  17033  firest  17484  fncnvimaeqv  18175  mgmhmpropd  18755  mhmpropd  18849  efmnd1bas  18951  subgacs  19226  ecxpid  19241  qsxpid  19242  eqgid  19247  ghmmhmb  19296  ghmpropd  19325  ghmqusnsglem1  19349  ghmquskerlem1  19352  ghmqusker  19356  resscntz  19402  symg1bas  19460  lsmcom2  19724  lsmass  19738  ablnsg  19916  lsmcomx  19925  gsum2d2  20043  subgdmdprd  20105  dprd2d2  20115  2nsgsimpgd  20173  unitpropd  20498  rnghmval2  20525  subsubrng2  20648  subrngpropd  20652  subsubrg2  20683  subrgpropd  20692  rhmpropd  20693  subrgacs  20880  sdrgacs  20881  abvpropd  20915  lssacs  21065  lssats2  21098  lsspropd  21115  lmhmpropd  21171  lbspropd  21197  pzriprnglem10  21608  psdmul  22297  discld  23214  neiptopnei  23257  neiptopreu  23258  restsn  23295  restdis  23303  neitr  23305  restlp  23308  cndis  23416  cnindis  23417  cnpdis  23418  lpcls  23489  hausmapdom  23625  ptpjpre1  23696  tx1cn  23734  tx2cn  23735  hauseqlcld  23771  txkgen  23777  idqtop  23831  tgqtop  23837  acufl  24042  uffix  24046  ufildr  24056  fmfg  24074  rnelfm  24078  fmfnfm  24083  fmid  24085  fmco  24086  flimrest  24108  fclsrest  24149  alexsubALT  24176  tsmsgsum  24264  tsmssubm  24268  tsmsres  24269  tsmsf1o  24270  xpsdsval  24506  blpnf  24522  blin  24546  blres  24556  xmetec  24559  imasf1obl  24613  imasf1oxms  24614  prdsbl  24616  metrest  24649  psmetutop  24692  restmetu  24695  dscopn  24698  cnbl0  24898  bl2ioo  24917  xrtgioo  24932  cncfmet  25036  icoopnst  25066  iocopnst  25067  cldcss2  25569  iunmbl2  25684  mbfmulc2lem  25774  mbfmax  25776  ismbf3d  25781  mbfimaopnlem  25782  mbfaddlem  25787  mbfsup  25791  i1f1lem  25816  i1faddlem  25820  i1fmullem  25821  i1fmulclem  25829  i1fres  25832  mbfi1fseqlem4  25845  limcdif  26003  limcnlp  26005  limcflf  26008  limcres  26013  limcun  26022  ply1remlem  26290  fta1glem2  26294  plypf1  26337  ofmulrt  26408  plyremlem  26433  aannenlem1  26457  gausslemma2dlem1a  27494  oldlim  28045  negleft  28216  negright  28217  tglineelsb2  28866  tglinecom  28869  ushgredgedg  29519  ushgredgedgloop  29521  nbumgrvtx  29636  nbusgrvtxm1uvtx  29695  vdiscusgr  29821  wspniunwspnon  30212  rusgrnumwwlkb0  30263  clwwlknscsh  30353  clwwlknun  30403  eupth2lems  30529  fusgr2wsp2nb  30625  fusgreg2wsp  30627  ubthlem1  31162  ocin  31588  shscom  31611  spansncol  31860  iunsnima  32903  iunsnima2  32904  nfpconfp  32917  unipreima  32928  2ndimaxp  32931  fdifsupp  32970  suppiniseg  32971  ressupprn  32975  1stpreimas  32991  1stpreima  32992  2ndpreima  32993  fpwrelmapffslem  33017  iocinioc2  33064  nndiffz1  33071  fzsplit3  33078  indf1ofs  33126  swrdrn3  33215  cntzun  33339  cntzsnid  33340  cntrval2  33431  lindspropd  33639  lsmsnpridl  33652  lsmssass  33654  grplsm0l  33655  grplsmid  33656  nsgqusf1olem2  33666  nsgqusf1olem3  33667  crngmxidl  33696  opprlidlabs  33711  rprmirredb  33766  ressply1mon1p  33802  fldextrspunlsp  34008  irngnzply1  34025  smatrcl  34130  qtophaus  34170  locfinreflem  34174  rspectopn  34201  zarclsiin  34205  rhmpreimacnlem  34218  prsdm  34248  prsrn  34249  1stmbfm  34594  2ndmbfm  34595  mbfmcnt  34602  eulerpartlemgh  34712  dstfrvunirn  34809  reprsuc  34946  reprpmtf1o  34957  satfvsucsuc  35755  dmopab3rexdif  35795  cbvabdavw  36656  neifg  36770  filnetlem4  36780  ontgval  36830  bj-gabima  37463  bj-restsn  37611  bj-rest10  37617  bj-restpw  37621  bj-restuni  37626  mptsnunlem  37871  finxpsuclem  37930  wl-clabtv  38128  wl-clabt  38129  poimirlem16  38174  poimirlem19  38177  poimirlem23  38181  poimirlem27  38185  heicant  38193  istotbnd3  38309  sstotbnd  38313  ismtyima  38341  heibor  38359  divrngidl  38566  eccnvep  38826  ecxrn  38944  eqvrelth  39233  disjlem19  39442  prtlem19  39541  prter2  39544  lkrsc  39760  lshpkr  39780  paddvaln0N  40464  paddval0  40473  diaglbN  41718  cdlemm10N  41781  lcfrvalsnN  42204  lcfrlem9  42213  lcdlss  42282  mapd1o  42311  mapd0  42328  hlhillcs  42621  grpods  42850  unitscyglem2  42852  sn-iotalem  42881  fsuppind  43213  mzpmfp  43369  lzunuz  43390  fz1eqin  43391  jm2.23  43614  pw2f1ocnv  43655  dfacbasgrp  43726  nnoeomeqom  43930  oadif1lem  43997  oadif1  43998  fzunt  44072  fzuntd  44073  fzunt1d  44074  fzuntgd  44075  inintabd  44196  cnvcnvintabd  44217  cnvintabd  44220  rfcnpre3  45644  rfcnpre4  45645  iindif2f  45769  rnmptpr  45786  iccshift  46125  iocopn  46127  iooshift  46129  iccintsng  46130  icoopn  46132  limcdm0  46225  limcresiooub  46247  limcresioolb  46248  fperdvper  46524  itgperiod  46586  fourierdlem32  46744  fourierdlem33  46745  fourierdlem48  46759  fourierdlem49  46760  fourierdlem81  46792  fsetsniunop  47674  elsetpreimafvrab  48031  iccpartiun  48071  dfclnbgr6  48509  dfnbgr6  48510  uhgrimisgrgric  48584  clnbgrgrim  48587  stgredgiun  48611  gpgnbgrvtx0  48727  gpgnbgrvtx1  48728  itsclinecirc0in  49439  i0oii  49582  io1ii  49583  sectpropd  49699  invpropd  49701  isopropd  49703  cicpropd  49712  uobffth  49880  uobeqw  49881  natoppfb  49893  oppc1stflem  49949  thincmon  50095  thincepi  50096  termfucterm  50206  grptcmon  50255  grptcepi  50256  lanval2  50289  ranval2  50292  ranval3  50293