Theorem eqrdv 2731

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 1931	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3		dfcleq 2726	. 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	2, 3	sylibr 233	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  eqrdav  2732  abbi  2801  eqabdv  2868  ss2abdv  4061  uneq1  4157  unineq  4278  difin2  4292  difsn  4802  intmin4  4982  iunconst  5007  iinconst  5008  iuneqconst  5009  dfiun2g  5034  dfiun2gOLD  5035  iindif1  5079  iindif2  5081  iinin2  5082  iunxsng  5094  iunxsngf  5096  opthprc  5741  dmopab2rex  5918  epin  6095  inimasn  6156  dmsnopg  6213  dfco2a  6246  iotaeq  6509  imadif  6633  unima  6967  ssimaex  6977  unpreima  7065  respreima  7068  iinpreima  7071  fnsnb  7164  fmptsng  7166  fmptsnd  7167  tpres  7202  iunpw  7758  ordpwsuc  7803  ordsucun  7813  fiun  7929  f1iun  7930  reldm  8030  fimaproj  8121  xpord2pred  8131  xpord3pred  8138  rntpos  8224  onoviun  8343  oarec  8562  iserd  8729  erth  8752  mapdm0  8836  mapfset  8844  ixpiin  8918  boxriin  8934  pw2f1olem  9076  fifo  9427  ordiso2  9510  ttrclse  9722  finacn  10045  acnen  10048  acacni  10135  dfac13  10137  fin23lem26  10320  isf34lem4  10372  axdc3lem2  10446  fpwwe2lem7  10632  fpwwe2lem11  10636  fpwwe2lem12  10637  gch2  10670  gchac  10676  gchina  10694  genpass  11004  1idpr  11024  eqreznegel  12918  ixxun  13340  iccid  13369  difreicc  13461  iccsplit  13462  fzsplit2  13526  fzsn  13543  fzpr  13556  uzsplit  13573  preduz  13623  predfz  13626  fz1isolem  14422  pr2pwpr  14440  isercolllem2  15612  isercoll  15614  bitsmod  16377  bitscmp  16379  saddisj  16406  sadadd  16408  sadass  16412  smupvallem  16424  smueqlem  16431  smumul  16434  gcdcllem2  16441  vdwapun  16907  firest  17378  fncnvimaeqv  18071  mhmpropd  18678  efmnd1bas  18774  subgacs  19041  eqgid  19060  ghmmhmb  19103  ghmpropd  19130  resscntz  19197  symg1bas  19258  lsmcom2  19523  lsmass  19537  ablnsg  19715  lsmcomx  19724  gsum2d2  19842  subgdmdprd  19904  dprd2d2  19914  2nsgsimpgd  19972  unitpropd  20231  subsubrg2  20346  subrgpropd  20355  rhmpropd  20356  subrgacs  20416  sdrgacs  20417  abvpropd  20450  lssacs  20578  lssats2  20611  lsspropd  20628  lmhmpropd  20684  lbspropd  20710  discld  22593  neiptopnei  22636  neiptopreu  22637  restsn  22674  restdis  22682  neitr  22684  restlp  22687  cndis  22795  cnindis  22796  cnpdis  22797  lpcls  22868  hausmapdom  23004  ptpjpre1  23075  tx1cn  23113  tx2cn  23114  hauseqlcld  23150  txkgen  23156  idqtop  23210  tgqtop  23216  acufl  23421  uffix  23425  ufildr  23435  fmfg  23453  rnelfm  23457  fmfnfm  23462  fmid  23464  fmco  23465  flimrest  23487  fclsrest  23528  alexsubALT  23555  tsmsgsum  23643  tsmssubm  23647  tsmsres  23648  tsmsf1o  23649  xpsdsval  23887  blpnf  23903  blin  23927  blres  23937  xmetec  23940  imasf1obl  23997  imasf1oxms  23998  prdsbl  24000  metrest  24033  psmetutop  24076  restmetu  24079  dscopn  24082  cnbl0  24290  bl2ioo  24308  xrtgioo  24322  cncfmet  24425  icoopnst  24455  iocopnst  24456  cldcss2  24959  iunmbl2  25074  mbfmulc2lem  25164  mbfmax  25166  ismbf3d  25171  mbfimaopnlem  25172  mbfaddlem  25177  mbfsup  25181  i1f1lem  25206  i1faddlem  25210  i1fmullem  25211  i1fmulclem  25220  i1fres  25223  mbfi1fseqlem4  25236  limcdif  25393  limcnlp  25395  limcflf  25398  limcres  25403  limcun  25412  ply1remlem  25680  fta1glem2  25684  plypf1  25726  ofmulrt  25795  plyremlem  25817  aannenlem1  25841  gausslemma2dlem1a  26868  oldlim  27382  tglineelsb2  27914  tglinecom  27917  ushgredgedg  28517  ushgredgedgloop  28519  nbumgrvtx  28634  nbusgrvtxm1uvtx  28693  vdiscusgr  28819  wspniunwspnon  29208  rusgrnumwwlkb0  29256  clwwlknscsh  29346  clwwlknun  29396  eupth2lems  29522  fusgr2wsp2nb  29618  fusgreg2wsp  29620  ubthlem1  30154  ocin  30580  shscom  30603  spansncol  30852  eqsnd  31797  iunsnima  31878  iunsnima2  31879  nfpconfp  31887  unipreima  31900  2ndimaxp  31903  suppiniseg  31939  ressupprn  31943  1stpreimas  31958  1stpreima  31959  2ndpreima  31960  fpwrelmapffslem  31988  iocinioc2  32021  nndiffz1  32028  fzsplit3  32036  swrdrn3  32150  cntzun  32243  cntzsnid  32244  ecxpid  32503  qsxpid  32505  lindspropd  32530  lsmsnpridl  32539  lsmssass  32543  grplsm0l  32544  grplsmid  32545  nsgqusf1olem2  32556  nsgqusf1olem3  32557  ghmquskerlem1  32559  ghmqusker  32563  crngmxidl  32616  opprlidlabs  32630  ressply1mon1p  32688  irngnzply1  32786  smatrcl  32807  qtophaus  32847  locfinreflem  32851  rspectopn  32878  zarclsiin  32882  rhmpreimacnlem  32895  prsdm  32925  prsrn  32926  indpi1  33049  indf1ofs  33055  1stmbfm  33290  2ndmbfm  33291  mbfmcnt  33298  eulerpartlemgh  33408  dstfrvunirn  33504  reprsuc  33658  reprpmtf1o  33669  satfvsucsuc  34387  dmopab3rexdif  34427  neifg  35304  filnetlem4  35314  ontgval  35364  bj-gabima  35868  bj-restsn  36011  bj-rest10  36017  bj-restpw  36021  bj-restuni  36026  mptsnunlem  36267  finxpsuclem  36326  wl-clabtv  36507  wl-clabt  36508  poimirlem16  36552  poimirlem19  36555  poimirlem23  36559  poimirlem27  36563  heicant  36571  istotbnd3  36687  sstotbnd  36691  ismtyima  36719  heibor  36737  divrngidl  36944  eccnvep  37198  ecxrn  37305  eqvrelth  37529  disjlem19  37719  prtlem19  37796  prter2  37799  lkrsc  38015  lshpkr  38035  paddvaln0N  38720  paddval0  38729  diaglbN  39974  cdlemm10N  40037  lcfrvalsnN  40460  lcfrlem9  40469  lcdlss  40538  mapd1o  40567  mapd0  40584  hlhillcs  40881  sn-iotalem  41086  fnsnbt  41099  fsuppind  41210  mzpmfp  41533  lzunuz  41554  fz1eqin  41555  jm2.23  41783  pw2f1ocnv  41824  dfacbasgrp  41898  nnoeomeqom  42110  oadif1lem  42177  oadif1  42178  fzunt  42254  fzuntd  42255  fzunt1d  42256  fzuntgd  42257  inintabd  42378  cnvcnvintabd  42399  cnvintabd  42402  rfcnpre3  43765  rfcnpre4  43766  iindif2f  43902  rnmptpr  43921  iccshift  44279  iocopn  44281  iooshift  44283  iccintsng  44284  icoopn  44286  limcdm0  44382  limcresiooub  44406  limcresioolb  44407  fperdvper  44683  itgperiod  44745  fourierdlem32  44903  fourierdlem33  44904  fourierdlem48  44918  fourierdlem49  44919  fourierdlem81  44951  fsetsniunop  45807  elsetpreimafvrab  46110  iccpartiun  46150  mgmhmpropd  46603  rnghmval2  46741  subsubrng2  46791  subrngpropd  46795  pzriprnglem10  46862  itsclinecirc0in  47509  i0oii  47600  io1ii  47601  thincmon  47702  thincepi  47703  grptcmon  47764  grptcepi  47765