Theorem eqrdv 2736

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  eqrdav  2737  abbi1  2807  abbi2dv  2876  ss2abdv  3993  uneq1  4086  unineq  4208  difin2  4222  difsn  4728  intmin4  4905  iunconst  4930  iinconst  4931  iuneqconst  4932  dfiun2g  4957  iindif1  5000  iindif2  5002  iinin2  5003  iunxsng  5015  iunxsngf  5017  opthprc  5642  dmopab2rex  5815  epin  5992  inimasn  6048  dmsnopg  6105  dfco2a  6139  iotaeq  6389  imadif  6502  unima  6825  ssimaex  6835  unpreima  6922  respreima  6925  iinpreima  6928  fnsnb  7020  fmptsng  7022  fmptsnd  7023  tpres  7058  iunpw  7599  ordpwsuc  7637  ordsucun  7647  fiun  7759  f1iun  7760  reldm  7858  fimaproj  7947  rntpos  8026  onoviun  8145  oarec  8355  iserd  8482  erth  8505  mapdm0  8588  mapfset  8596  ixpiin  8670  boxriin  8686  pw2f1olem  8816  fifo  9121  ordiso2  9204  finacn  9737  acnen  9740  acacni  9827  dfac13  9829  fin23lem26  10012  isf34lem4  10064  axdc3lem2  10138  fpwwe2lem7  10324  fpwwe2lem11  10328  fpwwe2lem12  10329  gch2  10362  gchac  10368  gchina  10386  genpass  10696  1idpr  10716  eqreznegel  12603  ixxun  13024  iccid  13053  difreicc  13145  iccsplit  13146  fzsplit2  13210  fzsn  13227  fzpr  13240  uzsplit  13257  preduz  13307  predfz  13310  fz1isolem  14103  pr2pwpr  14121  isercolllem2  15305  isercoll  15307  bitsmod  16071  bitscmp  16073  saddisj  16100  sadadd  16102  sadass  16106  smupvallem  16118  smueqlem  16125  smumul  16128  gcdcllem2  16135  vdwapun  16603  firest  17060  fncnvimaeqv  17752  mhmpropd  18351  efmnd1bas  18447  subgacs  18704  eqgid  18723  ghmmhmb  18760  ghmpropd  18787  resscntz  18853  symg1bas  18913  lsmcom2  19175  lsmass  19190  ablnsg  19363  lsmcomx  19372  gsum2d2  19490  subgdmdprd  19552  dprd2d2  19562  2nsgsimpgd  19620  unitpropd  19854  subsubrg2  19966  subrgpropd  19974  rhmpropd  19975  subrgacs  19983  sdrgacs  19984  abvpropd  20017  lssacs  20144  lssats2  20177  lsspropd  20194  lmhmpropd  20250  lbspropd  20276  discld  22148  neiptopnei  22191  neiptopreu  22192  restsn  22229  restdis  22237  neitr  22239  restlp  22242  cndis  22350  cnindis  22351  cnpdis  22352  lpcls  22423  hausmapdom  22559  ptpjpre1  22630  tx1cn  22668  tx2cn  22669  hauseqlcld  22705  txkgen  22711  idqtop  22765  tgqtop  22771  acufl  22976  uffix  22980  ufildr  22990  fmfg  23008  rnelfm  23012  fmfnfm  23017  fmid  23019  fmco  23020  flimrest  23042  fclsrest  23083  alexsubALT  23110  tsmsgsum  23198  tsmssubm  23202  tsmsres  23203  tsmsf1o  23204  xpsdsval  23442  blpnf  23458  blin  23482  blres  23492  xmetec  23495  imasf1obl  23550  imasf1oxms  23551  prdsbl  23553  metrest  23586  psmetutop  23629  restmetu  23632  dscopn  23635  cnbl0  23843  bl2ioo  23861  xrtgioo  23875  cncfmet  23978  icoopnst  24008  iocopnst  24009  cldcss2  24511  iunmbl2  24626  mbfmulc2lem  24716  mbfmax  24718  ismbf3d  24723  mbfimaopnlem  24724  mbfaddlem  24729  mbfsup  24733  i1f1lem  24758  i1faddlem  24762  i1fmullem  24763  i1fmulclem  24772  i1fres  24775  mbfi1fseqlem4  24788  limcdif  24945  limcnlp  24947  limcflf  24950  limcres  24955  limcun  24964  ply1remlem  25232  fta1glem2  25236  plypf1  25278  ofmulrt  25347  plyremlem  25369  aannenlem1  25393  gausslemma2dlem1a  26418  tglineelsb2  26897  tglinecom  26900  ushgredgedg  27499  ushgredgedgloop  27501  nbumgrvtx  27616  nbusgrvtxm1uvtx  27675  vdiscusgr  27801  wspniunwspnon  28189  rusgrnumwwlkb0  28237  clwwlknscsh  28327  clwwlknun  28377  eupth2lems  28503  fusgr2wsp2nb  28599  fusgreg2wsp  28601  ubthlem1  29133  ocin  29559  shscom  29582  spansncol  29831  eqsnd  30778  iunsnima  30859  iunsnima2  30860  nfpconfp  30868  unipreima  30882  2ndimaxp  30885  suppiniseg  30922  ressupprn  30926  1stpreimas  30940  1stpreima  30941  2ndpreima  30942  fpwrelmapffslem  30969  iocinioc2  31002  nndiffz1  31009  fzsplit3  31017  swrdrn3  31129  cntzun  31222  cntzsnid  31223  ecxpid  31458  qsxpid  31460  lindspropd  31479  lsmsnpridl  31488  lsmssass  31492  grplsm0l  31493  grplsmid  31494  nsgqusf1olem2  31501  nsgqusf1olem3  31502  smatrcl  31648  qtophaus  31688  locfinreflem  31692  rspectopn  31719  zarclsiin  31723  rhmpreimacnlem  31736  prsdm  31766  prsrn  31767  indpi1  31888  indf1ofs  31894  1stmbfm  32127  2ndmbfm  32128  mbfmcnt  32135  eulerpartlemgh  32245  dstfrvunirn  32341  reprsuc  32495  reprpmtf1o  32506  satfvsucsuc  33227  dmopab3rexdif  33267  ttrclse  33713  xpord2pred  33719  xpord3pred  33725  oldlim  33996  neifg  34487  filnetlem4  34497  ontgval  34547  bj-gabima  35055  bj-restsn  35180  bj-rest10  35186  bj-restpw  35190  bj-restuni  35195  mptsnunlem  35436  finxpsuclem  35495  wl-clabtv  35675  wl-clabt  35676  poimirlem16  35720  poimirlem19  35723  poimirlem23  35727  poimirlem27  35731  heicant  35739  istotbnd3  35856  sstotbnd  35860  ismtyima  35888  heibor  35906  divrngidl  36113  eccnvep  36344  ecxrn  36444  eqvrelth  36651  prtlem19  36819  prter2  36822  lkrsc  37038  lshpkr  37058  paddvaln0N  37742  paddval0  37751  diaglbN  38996  cdlemm10N  39059  lcfrvalsnN  39482  lcfrlem9  39491  lcdlss  39560  mapd1o  39589  mapd0  39606  hlhillcs  39903  sn-iotalem  40117  fnsnbt  40134  fsuppind  40202  mzpmfp  40485  lzunuz  40506  fz1eqin  40507  jm2.23  40734  pw2f1ocnv  40775  dfacbasgrp  40849  inintabd  41076  cnvcnvintabd  41097  cnvintabd  41100  rfcnpre3  42465  rfcnpre4  42466  rnmptpr  42602  iccshift  42946  iocopn  42948  iooshift  42950  iccintsng  42951  icoopn  42953  limcdm0  43049  limcresiooub  43073  limcresioolb  43074  fperdvper  43350  itgperiod  43412  fourierdlem32  43570  fourierdlem33  43571  fourierdlem48  43585  fourierdlem49  43586  fourierdlem81  43618  fsetsniunop  44430  elsetpreimafvrab  44734  iccpartiun  44774  mgmhmpropd  45227  rnghmval2  45341  itsclinecirc0in  46009  i0oii  46101  io1ii  46102  thincmon  46203  thincepi  46204  grptcmon  46263  grptcepi  46264