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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  eqrdav  2732  abbi  2798  eqabdv  2866  uneq1  4110  unineq  4237  difin2  4250  difsn  4751  eqsndOLD  4784  intmin4  4929  iunconst  4953  iinconst  4954  iuneqconst  4955  dfiun2g  4982  iindif1  5027  iindif2  5029  iinin2  5030  iunxsng  5042  iunxsngf  5044  opthprc  5685  dmopab2rex  5863  dmxp  5875  epin  6051  inimasn  6111  dmsnopg  6168  dfco2a  6201  iotaeq  6457  imadif  6573  unima  6906  ssimaex  6916  unpreima  7005  respreima  7008  iinpreima  7011  fnsnbg  7107  fnsnbOLD  7109  fmptsng  7111  fmptsnd  7112  tpres  7144  iunpw  7713  ordpwsuc  7754  ordsucun  7764  fiun  7884  f1iun  7885  reldm  7985  fimaproj  8074  xpord2pred  8084  xpord3pred  8091  rntpos  8178  onoviun  8272  oarec  8486  iserd  8657  erth  8685  mapdm0  8775  mapfset  8783  ixpiin  8858  boxriin  8874  pw2f1olem  9005  fifo  9327  ordiso2  9412  ttrclse  9628  finacn  9952  acnen  9955  acacni  10043  dfac13  10045  fin23lem26  10227  isf34lem4  10279  axdc3lem2  10353  fpwwe2lem7  10539  fpwwe2lem11  10543  fpwwe2lem12  10544  gch2  10577  gchac  10583  gchina  10601  genpass  10911  1idpr  10931  eqreznegel  12838  ixxun  13268  iccid  13297  difreicc  13391  iccsplit  13392  fzsplit2  13456  fzsn  13473  fzpr  13486  uzsplit  13503  fzdif1  13512  preduz  13557  predfz  13560  fz1isolem  14375  pr2pwpr  14393  isercolllem2  15580  isercoll  15582  bitsmod  16354  bitscmp  16356  saddisj  16383  sadadd  16385  sadass  16389  smupvallem  16401  smueqlem  16408  smumul  16411  gcdcllem2  16418  vdwapun  16893  firest  17343  fncnvimaeqv  18034  mgmhmpropd  18614  mhmpropd  18708  efmnd1bas  18809  subgacs  19081  eqgid  19100  ghmmhmb  19147  ghmpropd  19176  ghmqusnsglem1  19200  ghmquskerlem1  19203  ghmqusker  19207  resscntz  19253  symg1bas  19311  lsmcom2  19575  lsmass  19589  ablnsg  19767  lsmcomx  19776  gsum2d2  19894  subgdmdprd  19956  dprd2d2  19966  2nsgsimpgd  20024  unitpropd  20344  rnghmval2  20371  subsubrng2  20488  subrngpropd  20492  subsubrg2  20523  subrgpropd  20532  rhmpropd  20533  subrgacs  20724  sdrgacs  20725  abvpropd  20759  lssacs  20909  lssats2  20942  lsspropd  20960  lmhmpropd  21016  lbspropd  21042  pzriprnglem10  21436  psdmul  22100  discld  23024  neiptopnei  23067  neiptopreu  23068  restsn  23105  restdis  23113  neitr  23115  restlp  23118  cndis  23226  cnindis  23227  cnpdis  23228  lpcls  23299  hausmapdom  23435  ptpjpre1  23506  tx1cn  23544  tx2cn  23545  hauseqlcld  23581  txkgen  23587  idqtop  23641  tgqtop  23647  acufl  23852  uffix  23856  ufildr  23866  fmfg  23884  rnelfm  23888  fmfnfm  23893  fmid  23895  fmco  23896  flimrest  23918  fclsrest  23959  alexsubALT  23986  tsmsgsum  24074  tsmssubm  24078  tsmsres  24079  tsmsf1o  24080  xpsdsval  24316  blpnf  24332  blin  24356  blres  24366  xmetec  24369  imasf1obl  24423  imasf1oxms  24424  prdsbl  24426  metrest  24459  psmetutop  24502  restmetu  24505  dscopn  24508  cnbl0  24708  bl2ioo  24727  xrtgioo  24742  cncfmet  24849  icoopnst  24883  iocopnst  24884  cldcss2  25389  iunmbl2  25505  mbfmulc2lem  25595  mbfmax  25597  ismbf3d  25602  mbfimaopnlem  25603  mbfaddlem  25608  mbfsup  25612  i1f1lem  25637  i1faddlem  25641  i1fmullem  25642  i1fmulclem  25650  i1fres  25653  mbfi1fseqlem4  25666  limcdif  25824  limcnlp  25826  limcflf  25829  limcres  25834  limcun  25843  ply1remlem  26117  fta1glem2  26121  plypf1  26164  ofmulrt  26236  plyremlem  26259  aannenlem1  26283  gausslemma2dlem1a  27323  oldlim  27852  tglineelsb2  28630  tglinecom  28633  ushgredgedg  29228  ushgredgedgloop  29230  nbumgrvtx  29345  nbusgrvtxm1uvtx  29404  vdiscusgr  29531  wspniunwspnon  29922  rusgrnumwwlkb0  29973  clwwlknscsh  30063  clwwlknun  30113  eupth2lems  30239  fusgr2wsp2nb  30335  fusgreg2wsp  30337  ubthlem1  30871  ocin  31297  shscom  31320  spansncol  31569  iunsnima  32622  iunsnima2  32623  nfpconfp  32636  unipreima  32647  2ndimaxp  32650  fdifsupp  32690  suppiniseg  32691  ressupprn  32695  1stpreimas  32711  1stpreima  32712  2ndpreima  32713  fpwrelmapffslem  32739  iocinioc2  32787  nndiffz1  32794  fzsplit3  32801  indpi1  32869  indf1ofs  32876  swrdrn3  32965  cntzun  33089  cntzsnid  33090  cntrval2  33181  ecxpid  33370  qsxpid  33371  lindspropd  33392  lsmsnpridl  33407  lsmssass  33411  grplsm0l  33412  grplsmid  33413  nsgqusf1olem2  33423  nsgqusf1olem3  33424  crngmxidl  33478  opprlidlabs  33494  rprmirredb  33541  ressply1mon1p  33577  fldextrspunlsp  33759  irngnzply1  33776  smatrcl  33881  qtophaus  33921  locfinreflem  33925  rspectopn  33952  zarclsiin  33956  rhmpreimacnlem  33969  prsdm  33999  prsrn  34000  1stmbfm  34345  2ndmbfm  34346  mbfmcnt  34353  eulerpartlemgh  34463  dstfrvunirn  34560  reprsuc  34700  reprpmtf1o  34711  satfvsucsuc  35481  dmopab3rexdif  35521  cbvabdavw  36372  neifg  36487  filnetlem4  36497  ontgval  36547  bj-gabima  37057  bj-restsn  37199  bj-rest10  37205  bj-restpw  37209  bj-restuni  37214  mptsnunlem  37455  finxpsuclem  37514  wl-clabtv  37703  wl-clabt  37704  poimirlem16  37749  poimirlem19  37752  poimirlem23  37756  poimirlem27  37760  heicant  37768  istotbnd3  37884  sstotbnd  37888  ismtyima  37916  heibor  37934  divrngidl  38141  eccnvep  38393  ecxrn  38503  eqvrelth  38780  disjlem19  38972  prtlem19  39050  prter2  39053  lkrsc  39269  lshpkr  39289  paddvaln0N  39973  paddval0  39982  diaglbN  41227  cdlemm10N  41290  lcfrvalsnN  41713  lcfrlem9  41722  lcdlss  41791  mapd1o  41820  mapd0  41837  hlhillcs  42130  grpods  42360  unitscyglem2  42362  sn-iotalem  42392  fsuppind  42748  mzpmfp  42904  lzunuz  42925  fz1eqin  42926  jm2.23  43153  pw2f1ocnv  43194  dfacbasgrp  43265  nnoeomeqom  43469  oadif1lem  43536  oadif1  43537  fzunt  43612  fzuntd  43613  fzunt1d  43614  fzuntgd  43615  inintabd  43736  cnvcnvintabd  43757  cnvintabd  43760  rfcnpre3  45194  rfcnpre4  45195  iindif2f  45320  rnmptpr  45337  iccshift  45680  iocopn  45682  iooshift  45684  iccintsng  45685  icoopn  45687  limcdm0  45780  limcresiooub  45802  limcresioolb  45803  fperdvper  46079  itgperiod  46141  fourierdlem32  46299  fourierdlem33  46300  fourierdlem48  46314  fourierdlem49  46315  fourierdlem81  46347  fsetsniunop  47211  elsetpreimafvrab  47556  iccpartiun  47596  dfclnbgr6  48018  dfnbgr6  48019  uhgrimisgrgric  48093  clnbgrgrim  48096  stgredgiun  48120  gpgnbgrvtx0  48236  gpgnbgrvtx1  48237  itsclinecirc0in  48937  i0oii  49081  io1ii  49082  sectpropd  49198  invpropd  49200  isopropd  49202  cicpropd  49211  uobffth  49379  uobeqw  49380  natoppfb  49392  oppc1stflem  49448  thincmon  49594  thincepi  49595  termfucterm  49705  grptcmon  49754  grptcepi  49755  lanval2  49788  ranval2  49791  ranval3  49792