Theorem eqrdv 2735

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqrdav  2736  abbi  2802  eqabdv  2870  uneq1  4115  unineq  4242  difin2  4255  difsn  4756  eqsndOLD  4789  intmin4  4934  iunconst  4958  iinconst  4959  iuneqconst  4960  dfiun2g  4987  iindif1  5032  iindif2  5034  iinin2  5035  iunxsng  5047  iunxsngf  5049  opthprc  5696  dmopab2rex  5874  dmxp  5886  epin  6062  inimasn  6122  dmsnopg  6179  dfco2a  6212  iotaeq  6468  imadif  6584  unima  6917  ssimaex  6927  unpreima  7017  respreima  7020  iinpreima  7023  fnsnbg  7120  fnsnbOLD  7122  fmptsng  7124  fmptsnd  7125  tpres  7157  iunpw  7726  ordpwsuc  7767  ordsucun  7777  fiun  7897  f1iun  7898  reldm  7998  fimaproj  8087  xpord2pred  8097  xpord3pred  8104  rntpos  8191  onoviun  8285  oarec  8499  iserd  8672  erth  8700  mapdm0  8791  mapfset  8799  ixpiin  8874  boxriin  8890  pw2f1olem  9021  fifo  9347  ordiso2  9432  ttrclse  9648  finacn  9972  acnen  9975  acacni  10063  dfac13  10065  fin23lem26  10247  isf34lem4  10299  axdc3lem2  10373  fpwwe2lem7  10560  fpwwe2lem11  10564  fpwwe2lem12  10565  gch2  10598  gchac  10604  gchina  10622  genpass  10932  1idpr  10952  eqreznegel  12859  ixxun  13289  iccid  13318  difreicc  13412  iccsplit  13413  fzsplit2  13477  fzsn  13494  fzpr  13507  uzsplit  13524  fzdif1  13533  preduz  13578  predfz  13581  fz1isolem  14396  pr2pwpr  14414  isercolllem2  15601  isercoll  15603  bitsmod  16375  bitscmp  16377  saddisj  16404  sadadd  16406  sadass  16410  smupvallem  16422  smueqlem  16429  smumul  16432  gcdcllem2  16439  vdwapun  16914  firest  17364  fncnvimaeqv  18055  mgmhmpropd  18635  mhmpropd  18729  efmnd1bas  18830  subgacs  19102  eqgid  19121  ghmmhmb  19168  ghmpropd  19197  ghmqusnsglem1  19221  ghmquskerlem1  19224  ghmqusker  19228  resscntz  19274  symg1bas  19332  lsmcom2  19596  lsmass  19610  ablnsg  19788  lsmcomx  19797  gsum2d2  19915  subgdmdprd  19977  dprd2d2  19987  2nsgsimpgd  20045  unitpropd  20365  rnghmval2  20392  subsubrng2  20509  subrngpropd  20513  subsubrg2  20544  subrgpropd  20553  rhmpropd  20554  subrgacs  20745  sdrgacs  20746  abvpropd  20780  lssacs  20930  lssats2  20963  lsspropd  20981  lmhmpropd  21037  lbspropd  21063  pzriprnglem10  21457  psdmul  22121  discld  23045  neiptopnei  23088  neiptopreu  23089  restsn  23126  restdis  23134  neitr  23136  restlp  23139  cndis  23247  cnindis  23248  cnpdis  23249  lpcls  23320  hausmapdom  23456  ptpjpre1  23527  tx1cn  23565  tx2cn  23566  hauseqlcld  23602  txkgen  23608  idqtop  23662  tgqtop  23668  acufl  23873  uffix  23877  ufildr  23887  fmfg  23905  rnelfm  23909  fmfnfm  23914  fmid  23916  fmco  23917  flimrest  23939  fclsrest  23980  alexsubALT  24007  tsmsgsum  24095  tsmssubm  24099  tsmsres  24100  tsmsf1o  24101  xpsdsval  24337  blpnf  24353  blin  24377  blres  24387  xmetec  24390  imasf1obl  24444  imasf1oxms  24445  prdsbl  24447  metrest  24480  psmetutop  24523  restmetu  24526  dscopn  24529  cnbl0  24729  bl2ioo  24748  xrtgioo  24763  cncfmet  24870  icoopnst  24904  iocopnst  24905  cldcss2  25410  iunmbl2  25526  mbfmulc2lem  25616  mbfmax  25618  ismbf3d  25623  mbfimaopnlem  25624  mbfaddlem  25629  mbfsup  25633  i1f1lem  25658  i1faddlem  25662  i1fmullem  25663  i1fmulclem  25671  i1fres  25674  mbfi1fseqlem4  25687  limcdif  25845  limcnlp  25847  limcflf  25850  limcres  25855  limcun  25864  ply1remlem  26138  fta1glem2  26142  plypf1  26185  ofmulrt  26257  plyremlem  26280  aannenlem1  26304  gausslemma2dlem1a  27344  oldlim  27895  negleft  28066  negright  28067  tglineelsb2  28716  tglinecom  28719  ushgredgedg  29314  ushgredgedgloop  29316  nbumgrvtx  29431  nbusgrvtxm1uvtx  29490  vdiscusgr  29617  wspniunwspnon  30008  rusgrnumwwlkb0  30059  clwwlknscsh  30149  clwwlknun  30199  eupth2lems  30325  fusgr2wsp2nb  30421  fusgreg2wsp  30423  ubthlem1  30958  ocin  31384  shscom  31407  spansncol  31656  iunsnima  32708  iunsnima2  32709  nfpconfp  32722  unipreima  32733  2ndimaxp  32736  fdifsupp  32775  suppiniseg  32776  ressupprn  32780  1stpreimas  32796  1stpreima  32797  2ndpreima  32798  fpwrelmapffslem  32822  iocinioc2  32870  nndiffz1  32877  fzsplit3  32884  indpi1  32952  indf1ofs  32959  swrdrn3  33048  cntzun  33173  cntzsnid  33174  cntrval2  33265  ecxpid  33454  qsxpid  33455  lindspropd  33476  lsmsnpridl  33491  lsmssass  33495  grplsm0l  33496  grplsmid  33497  nsgqusf1olem2  33507  nsgqusf1olem3  33508  crngmxidl  33562  opprlidlabs  33578  rprmirredb  33625  ressply1mon1p  33661  fldextrspunlsp  33852  irngnzply1  33869  smatrcl  33974  qtophaus  34014  locfinreflem  34018  rspectopn  34045  zarclsiin  34049  rhmpreimacnlem  34062  prsdm  34092  prsrn  34093  1stmbfm  34438  2ndmbfm  34439  mbfmcnt  34446  eulerpartlemgh  34556  dstfrvunirn  34653  reprsuc  34793  reprpmtf1o  34804  satfvsucsuc  35581  dmopab3rexdif  35621  cbvabdavw  36472  neifg  36587  filnetlem4  36597  ontgval  36647  bj-gabima  37188  bj-restsn  37335  bj-rest10  37341  bj-restpw  37345  bj-restuni  37350  mptsnunlem  37593  finxpsuclem  37652  wl-clabtv  37841  wl-clabt  37842  poimirlem16  37887  poimirlem19  37890  poimirlem23  37894  poimirlem27  37898  heicant  37906  istotbnd3  38022  sstotbnd  38026  ismtyima  38054  heibor  38072  divrngidl  38279  eccnvep  38539  ecxrn  38657  eqvrelth  38946  disjlem19  39155  prtlem19  39254  prter2  39257  lkrsc  39473  lshpkr  39493  paddvaln0N  40177  paddval0  40186  diaglbN  41431  cdlemm10N  41494  lcfrvalsnN  41917  lcfrlem9  41926  lcdlss  41995  mapd1o  42024  mapd0  42041  hlhillcs  42334  grpods  42564  unitscyglem2  42566  sn-iotalem  42593  fsuppind  42948  mzpmfp  43104  lzunuz  43125  fz1eqin  43126  jm2.23  43353  pw2f1ocnv  43394  dfacbasgrp  43465  nnoeomeqom  43669  oadif1lem  43736  oadif1  43737  fzunt  43811  fzuntd  43812  fzunt1d  43813  fzuntgd  43814  inintabd  43935  cnvcnvintabd  43956  cnvintabd  43959  rfcnpre3  45393  rfcnpre4  45394  iindif2f  45519  rnmptpr  45536  iccshift  45878  iocopn  45880  iooshift  45882  iccintsng  45883  icoopn  45885  limcdm0  45978  limcresiooub  46000  limcresioolb  46001  fperdvper  46277  itgperiod  46339  fourierdlem32  46497  fourierdlem33  46498  fourierdlem48  46512  fourierdlem49  46513  fourierdlem81  46545  fsetsniunop  47409  elsetpreimafvrab  47754  iccpartiun  47794  dfclnbgr6  48216  dfnbgr6  48217  uhgrimisgrgric  48291  clnbgrgrim  48294  stgredgiun  48318  gpgnbgrvtx0  48434  gpgnbgrvtx1  48435  itsclinecirc0in  49135  i0oii  49279  io1ii  49280  sectpropd  49396  invpropd  49398  isopropd  49400  cicpropd  49409  uobffth  49577  uobeqw  49578  natoppfb  49590  oppc1stflem  49646  thincmon  49792  thincepi  49793  termfucterm  49903  grptcmon  49952  grptcepi  49953  lanval2  49986  ranval2  49989  ranval3  49990