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  27381  tglineelsb2  27883  tglinecom  27886  ushgredgedg  28486  ushgredgedgloop  28488  nbumgrvtx  28603  nbusgrvtxm1uvtx  28662  vdiscusgr  28788  wspniunwspnon  29177  rusgrnumwwlkb0  29225  clwwlknscsh  29315  clwwlknun  29365  eupth2lems  29491  fusgr2wsp2nb  29587  fusgreg2wsp  29589  ubthlem1  30123  ocin  30549  shscom  30572  spansncol  30821  eqsnd  31766  iunsnima  31847  iunsnima2  31848  nfpconfp  31856  unipreima  31869  2ndimaxp  31872  suppiniseg  31908  ressupprn  31912  1stpreimas  31927  1stpreima  31928  2ndpreima  31929  fpwrelmapffslem  31957  iocinioc2  31990  nndiffz1  31997  fzsplit3  32005  swrdrn3  32119  cntzun  32212  cntzsnid  32213  ecxpid  32472  qsxpid  32474  lindspropd  32499  lsmsnpridl  32508  lsmssass  32512  grplsm0l  32513  grplsmid  32514  nsgqusf1olem2  32525  nsgqusf1olem3  32526  ghmquskerlem1  32528  ghmqusker  32532  crngmxidl  32585  opprlidlabs  32599  ressply1mon1p  32657  irngnzply1  32755  smatrcl  32776  qtophaus  32816  locfinreflem  32820  rspectopn  32847  zarclsiin  32851  rhmpreimacnlem  32864  prsdm  32894  prsrn  32895  indpi1  33018  indf1ofs  33024  1stmbfm  33259  2ndmbfm  33260  mbfmcnt  33267  eulerpartlemgh  33377  dstfrvunirn  33473  reprsuc  33627  reprpmtf1o  33638  satfvsucsuc  34356  dmopab3rexdif  34396  neifg  35256  filnetlem4  35266  ontgval  35316  bj-gabima  35820  bj-restsn  35963  bj-rest10  35969  bj-restpw  35973  bj-restuni  35978  mptsnunlem  36219  finxpsuclem  36278  wl-clabtv  36459  wl-clabt  36460  poimirlem16  36504  poimirlem19  36507  poimirlem23  36511  poimirlem27  36515  heicant  36523  istotbnd3  36639  sstotbnd  36643  ismtyima  36671  heibor  36689  divrngidl  36896  eccnvep  37150  ecxrn  37257  eqvrelth  37481  disjlem19  37671  prtlem19  37748  prter2  37751  lkrsc  37967  lshpkr  37987  paddvaln0N  38672  paddval0  38681  diaglbN  39926  cdlemm10N  39989  lcfrvalsnN  40412  lcfrlem9  40421  lcdlss  40490  mapd1o  40519  mapd0  40536  hlhillcs  40833  sn-iotalem  41038  fnsnbt  41051  fsuppind  41162  mzpmfp  41485  lzunuz  41506  fz1eqin  41507  jm2.23  41735  pw2f1ocnv  41776  dfacbasgrp  41850  nnoeomeqom  42062  oadif1lem  42129  oadif1  42130  fzunt  42206  fzuntd  42207  fzunt1d  42208  fzuntgd  42209  inintabd  42330  cnvcnvintabd  42351  cnvintabd  42354  rfcnpre3  43717  rfcnpre4  43718  iindif2f  43854  rnmptpr  43873  iccshift  44231  iocopn  44233  iooshift  44235  iccintsng  44236  icoopn  44238  limcdm0  44334  limcresiooub  44358  limcresioolb  44359  fperdvper  44635  itgperiod  44697  fourierdlem32  44855  fourierdlem33  44856  fourierdlem48  44870  fourierdlem49  44871  fourierdlem81  44903  fsetsniunop  45759  elsetpreimafvrab  46062  iccpartiun  46102  mgmhmpropd  46555  rnghmval2  46693  subsubrng2  46743  subrngpropd  46747  pzriprnglem10  46814  itsclinecirc0in  47461  i0oii  47552  io1ii  47553  thincmon  47654  thincepi  47655  grptcmon  47716  grptcepi  47717