Theorem eqrdv 2734

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 2729	. 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 2708

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

This theorem is referenced by:  eqrdav  2735  abbi  2801  eqabdv  2869  uneq1  4113  unineq  4240  difin2  4253  difsn  4754  eqsndOLD  4787  intmin4  4932  iunconst  4956  iinconst  4957  iuneqconst  4958  dfiun2g  4985  iindif1  5030  iindif2  5032  iinin2  5033  iunxsng  5045  iunxsngf  5047  opthprc  5688  dmopab2rex  5866  dmxp  5878  epin  6054  inimasn  6114  dmsnopg  6171  dfco2a  6204  iotaeq  6460  imadif  6576  unima  6909  ssimaex  6919  unpreima  7008  respreima  7011  iinpreima  7014  fnsnbg  7110  fnsnbOLD  7112  fmptsng  7114  fmptsnd  7115  tpres  7147  iunpw  7716  ordpwsuc  7757  ordsucun  7767  fiun  7887  f1iun  7888  reldm  7988  fimaproj  8077  xpord2pred  8087  xpord3pred  8094  rntpos  8181  onoviun  8275  oarec  8489  iserd  8661  erth  8689  mapdm0  8779  mapfset  8787  ixpiin  8862  boxriin  8878  pw2f1olem  9009  fifo  9335  ordiso2  9420  ttrclse  9636  finacn  9960  acnen  9963  acacni  10051  dfac13  10053  fin23lem26  10235  isf34lem4  10287  axdc3lem2  10361  fpwwe2lem7  10548  fpwwe2lem11  10552  fpwwe2lem12  10553  gch2  10586  gchac  10592  gchina  10610  genpass  10920  1idpr  10940  eqreznegel  12847  ixxun  13277  iccid  13306  difreicc  13400  iccsplit  13401  fzsplit2  13465  fzsn  13482  fzpr  13495  uzsplit  13512  fzdif1  13521  preduz  13566  predfz  13569  fz1isolem  14384  pr2pwpr  14402  isercolllem2  15589  isercoll  15591  bitsmod  16363  bitscmp  16365  saddisj  16392  sadadd  16394  sadass  16398  smupvallem  16410  smueqlem  16417  smumul  16420  gcdcllem2  16427  vdwapun  16902  firest  17352  fncnvimaeqv  18043  mgmhmpropd  18623  mhmpropd  18717  efmnd1bas  18818  subgacs  19090  eqgid  19109  ghmmhmb  19156  ghmpropd  19185  ghmqusnsglem1  19209  ghmquskerlem1  19212  ghmqusker  19216  resscntz  19262  symg1bas  19320  lsmcom2  19584  lsmass  19598  ablnsg  19776  lsmcomx  19785  gsum2d2  19903  subgdmdprd  19965  dprd2d2  19975  2nsgsimpgd  20033  unitpropd  20353  rnghmval2  20380  subsubrng2  20497  subrngpropd  20501  subsubrg2  20532  subrgpropd  20541  rhmpropd  20542  subrgacs  20733  sdrgacs  20734  abvpropd  20768  lssacs  20918  lssats2  20951  lsspropd  20969  lmhmpropd  21025  lbspropd  21051  pzriprnglem10  21445  psdmul  22109  discld  23033  neiptopnei  23076  neiptopreu  23077  restsn  23114  restdis  23122  neitr  23124  restlp  23127  cndis  23235  cnindis  23236  cnpdis  23237  lpcls  23308  hausmapdom  23444  ptpjpre1  23515  tx1cn  23553  tx2cn  23554  hauseqlcld  23590  txkgen  23596  idqtop  23650  tgqtop  23656  acufl  23861  uffix  23865  ufildr  23875  fmfg  23893  rnelfm  23897  fmfnfm  23902  fmid  23904  fmco  23905  flimrest  23927  fclsrest  23968  alexsubALT  23995  tsmsgsum  24083  tsmssubm  24087  tsmsres  24088  tsmsf1o  24089  xpsdsval  24325  blpnf  24341  blin  24365  blres  24375  xmetec  24378  imasf1obl  24432  imasf1oxms  24433  prdsbl  24435  metrest  24468  psmetutop  24511  restmetu  24514  dscopn  24517  cnbl0  24717  bl2ioo  24736  xrtgioo  24751  cncfmet  24858  icoopnst  24892  iocopnst  24893  cldcss2  25398  iunmbl2  25514  mbfmulc2lem  25604  mbfmax  25606  ismbf3d  25611  mbfimaopnlem  25612  mbfaddlem  25617  mbfsup  25621  i1f1lem  25646  i1faddlem  25650  i1fmullem  25651  i1fmulclem  25659  i1fres  25662  mbfi1fseqlem4  25675  limcdif  25833  limcnlp  25835  limcflf  25838  limcres  25843  limcun  25852  ply1remlem  26126  fta1glem2  26130  plypf1  26173  ofmulrt  26245  plyremlem  26268  aannenlem1  26292  gausslemma2dlem1a  27332  oldlim  27883  negleft  28054  negright  28055  tglineelsb2  28704  tglinecom  28707  ushgredgedg  29302  ushgredgedgloop  29304  nbumgrvtx  29419  nbusgrvtxm1uvtx  29478  vdiscusgr  29605  wspniunwspnon  29996  rusgrnumwwlkb0  30047  clwwlknscsh  30137  clwwlknun  30187  eupth2lems  30313  fusgr2wsp2nb  30409  fusgreg2wsp  30411  ubthlem1  30945  ocin  31371  shscom  31394  spansncol  31643  iunsnima  32696  iunsnima2  32697  nfpconfp  32710  unipreima  32721  2ndimaxp  32724  fdifsupp  32764  suppiniseg  32765  ressupprn  32769  1stpreimas  32785  1stpreima  32786  2ndpreima  32787  fpwrelmapffslem  32811  iocinioc2  32859  nndiffz1  32866  fzsplit3  32873  indpi1  32941  indf1ofs  32948  swrdrn3  33037  cntzun  33161  cntzsnid  33162  cntrval2  33253  ecxpid  33442  qsxpid  33443  lindspropd  33464  lsmsnpridl  33479  lsmssass  33483  grplsm0l  33484  grplsmid  33485  nsgqusf1olem2  33495  nsgqusf1olem3  33496  crngmxidl  33550  opprlidlabs  33566  rprmirredb  33613  ressply1mon1p  33649  fldextrspunlsp  33831  irngnzply1  33848  smatrcl  33953  qtophaus  33993  locfinreflem  33997  rspectopn  34024  zarclsiin  34028  rhmpreimacnlem  34041  prsdm  34071  prsrn  34072  1stmbfm  34417  2ndmbfm  34418  mbfmcnt  34425  eulerpartlemgh  34535  dstfrvunirn  34632  reprsuc  34772  reprpmtf1o  34783  satfvsucsuc  35559  dmopab3rexdif  35599  cbvabdavw  36450  neifg  36565  filnetlem4  36575  ontgval  36625  bj-gabima  37141  bj-restsn  37287  bj-rest10  37293  bj-restpw  37297  bj-restuni  37302  mptsnunlem  37543  finxpsuclem  37602  wl-clabtv  37791  wl-clabt  37792  poimirlem16  37837  poimirlem19  37840  poimirlem23  37844  poimirlem27  37848  heicant  37856  istotbnd3  37972  sstotbnd  37976  ismtyima  38004  heibor  38022  divrngidl  38229  eccnvep  38481  ecxrn  38591  eqvrelth  38868  disjlem19  39060  prtlem19  39138  prter2  39141  lkrsc  39357  lshpkr  39377  paddvaln0N  40061  paddval0  40070  diaglbN  41315  cdlemm10N  41378  lcfrvalsnN  41801  lcfrlem9  41810  lcdlss  41879  mapd1o  41908  mapd0  41925  hlhillcs  42218  grpods  42448  unitscyglem2  42450  sn-iotalem  42477  fsuppind  42833  mzpmfp  42989  lzunuz  43010  fz1eqin  43011  jm2.23  43238  pw2f1ocnv  43279  dfacbasgrp  43350  nnoeomeqom  43554  oadif1lem  43621  oadif1  43622  fzunt  43696  fzuntd  43697  fzunt1d  43698  fzuntgd  43699  inintabd  43820  cnvcnvintabd  43841  cnvintabd  43844  rfcnpre3  45278  rfcnpre4  45279  iindif2f  45404  rnmptpr  45421  iccshift  45764  iocopn  45766  iooshift  45768  iccintsng  45769  icoopn  45771  limcdm0  45864  limcresiooub  45886  limcresioolb  45887  fperdvper  46163  itgperiod  46225  fourierdlem32  46383  fourierdlem33  46384  fourierdlem48  46398  fourierdlem49  46399  fourierdlem81  46431  fsetsniunop  47295  elsetpreimafvrab  47640  iccpartiun  47680  dfclnbgr6  48102  dfnbgr6  48103  uhgrimisgrgric  48177  clnbgrgrim  48180  stgredgiun  48204  gpgnbgrvtx0  48320  gpgnbgrvtx1  48321  itsclinecirc0in  49021  i0oii  49165  io1ii  49166  sectpropd  49282  invpropd  49284  isopropd  49286  cicpropd  49295  uobffth  49463  uobeqw  49464  natoppfb  49476  oppc1stflem  49532  thincmon  49678  thincepi  49679  termfucterm  49789  grptcmon  49838  grptcepi  49839  lanval2  49872  ranval2  49875  ranval3  49876