Theorem eqrdv 2737

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

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  eqrdav  2738  abbi  2804  eqabdv  2872  uneq1  4091  unineq  4216  difin2  4229  difsn  4731  eqsndOLD  4762  intmin4  4907  intprg  4911  iunconst  4931  iinconst  4932  iuneqconst  4933  dfiun2g  4959  iindif1  5004  iindif2  5006  iinin2  5007  iunxsng  5019  iunxsngf  5021  opthprc  5682  dmopab2rex  5859  dmxp  5871  epin  6047  inimasn  6107  dmsnopg  6164  dfco2a  6197  iotaeq  6453  imadif  6569  unima  6902  ssimaex  6912  unpreima  7004  respreima  7007  iinpreima  7010  fnsnbg  7108  fnsnbOLD  7110  fmptsng  7112  fmptsnd  7113  tpres  7145  iunpw  7714  ordpwsuc  7755  ordsucun  7765  fiun  7885  f1iun  7886  reldm  7986  fimaproj  8075  xpord2pred  8085  xpord3pred  8092  rntpos  8179  onoviun  8273  oarec  8487  iserd  8660  erth  8688  mapdm0  8779  mapfset  8787  ixpiin  8862  boxriin  8878  pw2f1olem  9009  fifo  9335  ordiso2  9420  ttrclse  9639  finacn  9963  acnen  9966  acacni  10054  dfac13  10056  fin23lem26  10238  isf34lem4  10290  axdc3lem2  10364  fpwwe2lem7  10551  fpwwe2lem11  10555  fpwwe2lem12  10556  gch2  10589  gchac  10595  gchina  10613  genpass  10923  1idpr  10943  indpi1  12164  eqreznegel  12875  ixxun  13305  iccid  13334  difreicc  13428  iccsplit  13429  fzsplit2  13494  fzsn  13511  fzpr  13524  uzsplit  13541  fzdif1  13550  preduz  13595  predfz  13598  fz1isolem  14414  pr2pwpr  14432  isercolllem2  15619  isercoll  15621  bitsmod  16396  bitscmp  16398  saddisj  16425  sadadd  16427  sadass  16431  smupvallem  16443  smueqlem  16450  smumul  16453  gcdcllem2  16460  vdwapun  16936  firest  17386  fncnvimaeqv  18077  mgmhmpropd  18657  mhmpropd  18751  efmnd1bas  18852  subgacs  19127  eqgid  19146  ghmmhmb  19193  ghmpropd  19222  ghmqusnsglem1  19246  ghmquskerlem1  19249  ghmqusker  19253  resscntz  19299  symg1bas  19357  lsmcom2  19621  lsmass  19635  ablnsg  19813  lsmcomx  19822  gsum2d2  19940  subgdmdprd  20002  dprd2d2  20012  2nsgsimpgd  20070  unitpropd  20388  rnghmval2  20415  subsubrng2  20536  subrngpropd  20540  subsubrg2  20571  subrgpropd  20580  rhmpropd  20581  subrgacs  20772  sdrgacs  20773  abvpropd  20807  lssacs  20957  lssats2  20990  lsspropd  21007  lmhmpropd  21063  lbspropd  21089  pzriprnglem10  21465  psdmul  22154  discld  23072  neiptopnei  23115  neiptopreu  23116  restsn  23153  restdis  23161  neitr  23163  restlp  23166  cndis  23274  cnindis  23275  cnpdis  23276  lpcls  23347  hausmapdom  23483  ptpjpre1  23554  tx1cn  23592  tx2cn  23593  hauseqlcld  23629  txkgen  23635  idqtop  23689  tgqtop  23695  acufl  23900  uffix  23904  ufildr  23914  fmfg  23932  rnelfm  23936  fmfnfm  23941  fmid  23943  fmco  23944  flimrest  23966  fclsrest  24007  alexsubALT  24034  tsmsgsum  24122  tsmssubm  24126  tsmsres  24127  tsmsf1o  24128  xpsdsval  24364  blpnf  24380  blin  24404  blres  24414  xmetec  24417  imasf1obl  24471  imasf1oxms  24472  prdsbl  24474  metrest  24507  psmetutop  24550  restmetu  24553  dscopn  24556  cnbl0  24756  bl2ioo  24775  xrtgioo  24790  cncfmet  24894  icoopnst  24924  iocopnst  24925  cldcss2  25427  iunmbl2  25542  mbfmulc2lem  25632  mbfmax  25634  ismbf3d  25639  mbfimaopnlem  25640  mbfaddlem  25645  mbfsup  25649  i1f1lem  25674  i1faddlem  25678  i1fmullem  25679  i1fmulclem  25687  i1fres  25690  mbfi1fseqlem4  25703  limcdif  25861  limcnlp  25863  limcflf  25866  limcres  25871  limcun  25880  ply1remlem  26148  fta1glem2  26152  plypf1  26195  ofmulrt  26266  plyremlem  26288  aannenlem1  26312  gausslemma2dlem1a  27346  oldlim  27897  negleft  28068  negright  28069  tglineelsb2  28718  tglinecom  28721  ushgredgedg  29316  ushgredgedgloop  29318  nbumgrvtx  29433  nbusgrvtxm1uvtx  29492  vdiscusgr  29618  wspniunwspnon  30009  rusgrnumwwlkb0  30060  clwwlknscsh  30150  clwwlknun  30200  eupth2lems  30326  fusgr2wsp2nb  30422  fusgreg2wsp  30424  ubthlem1  30959  ocin  31385  shscom  31408  spansncol  31657  iunsnima  32710  iunsnima2  32711  nfpconfp  32724  unipreima  32735  2ndimaxp  32738  fdifsupp  32777  suppiniseg  32778  ressupprn  32782  1stpreimas  32798  1stpreima  32799  2ndpreima  32800  fpwrelmapffslem  32824  iocinioc2  32871  nndiffz1  32878  fzsplit3  32885  indf1ofs  32945  swrdrn3  33034  cntzun  33160  cntzsnid  33161  cntrval2  33252  ecxpid  33444  qsxpid  33445  lindspropd  33466  lsmsnpridl  33481  lsmssass  33485  grplsm0l  33486  grplsmid  33487  nsgqusf1olem2  33497  nsgqusf1olem3  33498  crngmxidl  33552  opprlidlabs  33568  rprmirredb  33615  ressply1mon1p  33651  fldextrspunlsp  33858  irngnzply1  33875  smatrcl  33980  qtophaus  34020  locfinreflem  34024  rspectopn  34051  zarclsiin  34055  rhmpreimacnlem  34068  prsdm  34098  prsrn  34099  1stmbfm  34444  2ndmbfm  34445  mbfmcnt  34452  eulerpartlemgh  34562  dstfrvunirn  34659  reprsuc  34799  reprpmtf1o  34810  satfvsucsuc  35593  dmopab3rexdif  35633  cbvabdavw  36484  neifg  36599  filnetlem4  36609  ontgval  36659  bj-gabima  37293  bj-restsn  37440  bj-rest10  37446  bj-restpw  37450  bj-restuni  37455  mptsnunlem  37700  finxpsuclem  37759  wl-clabtv  37957  wl-clabt  37958  poimirlem16  38003  poimirlem19  38006  poimirlem23  38010  poimirlem27  38014  heicant  38022  istotbnd3  38138  sstotbnd  38142  ismtyima  38170  heibor  38188  divrngidl  38395  eccnvep  38655  ecxrn  38773  eqvrelth  39062  disjlem19  39271  prtlem19  39370  prter2  39373  lkrsc  39589  lshpkr  39609  paddvaln0N  40293  paddval0  40302  diaglbN  41547  cdlemm10N  41610  lcfrvalsnN  42033  lcfrlem9  42042  lcdlss  42111  mapd1o  42140  mapd0  42157  hlhillcs  42450  grpods  42679  unitscyglem2  42681  sn-iotalem  42708  fsuppind  43040  mzpmfp  43196  lzunuz  43217  fz1eqin  43218  jm2.23  43441  pw2f1ocnv  43482  dfacbasgrp  43553  nnoeomeqom  43757  oadif1lem  43824  oadif1  43825  fzunt  43899  fzuntd  43900  fzunt1d  43901  fzuntgd  43902  inintabd  44023  cnvcnvintabd  44044  cnvintabd  44047  rfcnpre3  45481  rfcnpre4  45482  iindif2f  45607  rnmptpr  45624  iccshift  45963  iocopn  45965  iooshift  45967  iccintsng  45968  icoopn  45970  limcdm0  46063  limcresiooub  46085  limcresioolb  46086  fperdvper  46362  itgperiod  46424  fourierdlem32  46582  fourierdlem33  46583  fourierdlem48  46597  fourierdlem49  46598  fourierdlem81  46630  fsetsniunop  47512  elsetpreimafvrab  47869  iccpartiun  47909  dfclnbgr6  48347  dfnbgr6  48348  uhgrimisgrgric  48422  clnbgrgrim  48425  stgredgiun  48449  gpgnbgrvtx0  48565  gpgnbgrvtx1  48566  itsclinecirc0in  49266  i0oii  49410  io1ii  49411  sectpropd  49527  invpropd  49529  isopropd  49531  cicpropd  49540  uobffth  49708  uobeqw  49709  natoppfb  49721  oppc1stflem  49777  thincmon  49923  thincepi  49924  termfucterm  50034  grptcmon  50083  grptcepi  50084  lanval2  50117  ranval2  50120  ranval3  50121