Theorem eqrdv 2738

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  eqrdav  2739  abbi  2810  eqabdv  2878  uneq1  4184  unineq  4307  difin2  4320  difsn  4823  eqsndOLD  4856  intmin4  5001  iunconst  5024  iinconst  5025  iuneqconst  5026  dfiun2g  5053  dfiun2gOLD  5054  iindif1  5098  iindif2  5100  iinin2  5101  iunxsng  5113  iunxsngf  5115  opthprc  5764  dmopab2rex  5942  dmxp  5953  epin  6125  inimasn  6187  dmsnopg  6244  dfco2a  6277  iotaeq  6538  imadif  6662  unima  6997  ssimaex  7007  unpreima  7096  respreima  7099  iinpreima  7102  fnsnb  7200  fmptsng  7202  fmptsnd  7203  tpres  7238  iunpw  7806  ordpwsuc  7851  ordsucun  7861  fiun  7983  f1iun  7984  reldm  8085  fimaproj  8176  xpord2pred  8186  xpord3pred  8193  rntpos  8280  onoviun  8399  oarec  8618  iserd  8789  erth  8814  mapdm0  8900  mapfset  8908  ixpiin  8982  boxriin  8998  pw2f1olem  9142  fifo  9501  ordiso2  9584  ttrclse  9796  finacn  10119  acnen  10122  acacni  10210  dfac13  10212  fin23lem26  10394  isf34lem4  10446  axdc3lem2  10520  fpwwe2lem7  10706  fpwwe2lem11  10710  fpwwe2lem12  10711  gch2  10744  gchac  10750  gchina  10768  genpass  11078  1idpr  11098  eqreznegel  12999  ixxun  13423  iccid  13452  difreicc  13544  iccsplit  13545  fzsplit2  13609  fzsn  13626  fzpr  13639  uzsplit  13656  preduz  13707  predfz  13710  fz1isolem  14510  pr2pwpr  14528  isercolllem2  15714  isercoll  15716  bitsmod  16482  bitscmp  16484  saddisj  16511  sadadd  16513  sadass  16517  smupvallem  16529  smueqlem  16536  smumul  16539  gcdcllem2  16546  vdwapun  17021  firest  17492  fncnvimaeqv  18188  mgmhmpropd  18736  mhmpropd  18827  efmnd1bas  18928  subgacs  19201  eqgid  19220  ghmmhmb  19267  ghmpropd  19296  ghmqusnsglem1  19320  ghmquskerlem1  19323  ghmqusker  19327  resscntz  19373  symg1bas  19432  lsmcom2  19697  lsmass  19711  ablnsg  19889  lsmcomx  19898  gsum2d2  20016  subgdmdprd  20078  dprd2d2  20088  2nsgsimpgd  20146  unitpropd  20443  rnghmval2  20470  subsubrng2  20590  subrngpropd  20594  subsubrg2  20627  subrgpropd  20636  rhmpropd  20637  subrgacs  20823  sdrgacs  20824  abvpropd  20858  lssacs  20988  lssats2  21021  lsspropd  21039  lmhmpropd  21095  lbspropd  21121  pzriprnglem10  21524  psdmul  22193  discld  23118  neiptopnei  23161  neiptopreu  23162  restsn  23199  restdis  23207  neitr  23209  restlp  23212  cndis  23320  cnindis  23321  cnpdis  23322  lpcls  23393  hausmapdom  23529  ptpjpre1  23600  tx1cn  23638  tx2cn  23639  hauseqlcld  23675  txkgen  23681  idqtop  23735  tgqtop  23741  acufl  23946  uffix  23950  ufildr  23960  fmfg  23978  rnelfm  23982  fmfnfm  23987  fmid  23989  fmco  23990  flimrest  24012  fclsrest  24053  alexsubALT  24080  tsmsgsum  24168  tsmssubm  24172  tsmsres  24173  tsmsf1o  24174  xpsdsval  24412  blpnf  24428  blin  24452  blres  24462  xmetec  24465  imasf1obl  24522  imasf1oxms  24523  prdsbl  24525  metrest  24558  psmetutop  24601  restmetu  24604  dscopn  24607  cnbl0  24815  bl2ioo  24833  xrtgioo  24847  cncfmet  24954  icoopnst  24988  iocopnst  24989  cldcss2  25495  iunmbl2  25611  mbfmulc2lem  25701  mbfmax  25703  ismbf3d  25708  mbfimaopnlem  25709  mbfaddlem  25714  mbfsup  25718  i1f1lem  25743  i1faddlem  25747  i1fmullem  25748  i1fmulclem  25757  i1fres  25760  mbfi1fseqlem4  25773  limcdif  25931  limcnlp  25933  limcflf  25936  limcres  25941  limcun  25950  ply1remlem  26224  fta1glem2  26228  plypf1  26271  ofmulrt  26341  plyremlem  26364  aannenlem1  26388  gausslemma2dlem1a  27427  oldlim  27943  tglineelsb2  28658  tglinecom  28661  ushgredgedg  29264  ushgredgedgloop  29266  nbumgrvtx  29381  nbusgrvtxm1uvtx  29440  vdiscusgr  29567  wspniunwspnon  29956  rusgrnumwwlkb0  30004  clwwlknscsh  30094  clwwlknun  30144  eupth2lems  30270  fusgr2wsp2nb  30366  fusgreg2wsp  30368  ubthlem1  30902  ocin  31328  shscom  31351  spansncol  31600  iunsnima  32640  iunsnima2  32641  nfpconfp  32651  unipreima  32662  2ndimaxp  32665  suppiniseg  32698  ressupprn  32702  1stpreimas  32717  1stpreima  32718  2ndpreima  32719  fpwrelmapffslem  32746  iocinioc2  32784  nndiffz1  32791  fzsplit3  32799  swrdrn3  32922  cntzun  33044  cntzsnid  33045  ecxpid  33354  qsxpid  33355  lindspropd  33376  lsmsnpridl  33391  lsmssass  33395  grplsm0l  33396  grplsmid  33397  nsgqusf1olem2  33407  nsgqusf1olem3  33408  crngmxidl  33462  opprlidlabs  33478  rprmirredb  33525  ressply1mon1p  33558  irngnzply1  33691  smatrcl  33742  qtophaus  33782  locfinreflem  33786  rspectopn  33813  zarclsiin  33817  rhmpreimacnlem  33830  prsdm  33860  prsrn  33861  indpi1  33984  indf1ofs  33990  1stmbfm  34225  2ndmbfm  34226  mbfmcnt  34233  eulerpartlemgh  34343  dstfrvunirn  34439  reprsuc  34592  reprpmtf1o  34603  satfvsucsuc  35333  dmopab3rexdif  35373  cbvabdavw  36222  neifg  36337  filnetlem4  36347  ontgval  36397  bj-gabima  36906  bj-restsn  37048  bj-rest10  37054  bj-restpw  37058  bj-restuni  37063  mptsnunlem  37304  finxpsuclem  37363  wl-clabtv  37551  wl-clabt  37552  poimirlem16  37596  poimirlem19  37599  poimirlem23  37603  poimirlem27  37607  heicant  37615  istotbnd3  37731  sstotbnd  37735  ismtyima  37763  heibor  37781  divrngidl  37988  eccnvep  38238  ecxrn  38343  eqvrelth  38567  disjlem19  38757  prtlem19  38834  prter2  38837  lkrsc  39053  lshpkr  39073  paddvaln0N  39758  paddval0  39767  diaglbN  41012  cdlemm10N  41075  lcfrvalsnN  41498  lcfrlem9  41507  lcdlss  41576  mapd1o  41605  mapd0  41622  hlhillcs  41919  grpods  42151  unitscyglem2  42153  sn-iotalem  42214  fnsnbt  42225  fsuppind  42545  mzpmfp  42703  lzunuz  42724  fz1eqin  42725  jm2.23  42953  pw2f1ocnv  42994  dfacbasgrp  43065  nnoeomeqom  43274  oadif1lem  43341  oadif1  43342  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  inintabd  43541  cnvcnvintabd  43562  cnvintabd  43565  rfcnpre3  44933  rfcnpre4  44934  iindif2f  45065  rnmptpr  45084  iccshift  45436  iocopn  45438  iooshift  45440  iccintsng  45441  icoopn  45443  limcdm0  45539  limcresiooub  45563  limcresioolb  45564  fperdvper  45840  itgperiod  45902  fourierdlem32  46060  fourierdlem33  46061  fourierdlem48  46075  fourierdlem49  46076  fourierdlem81  46108  fsetsniunop  46964  elsetpreimafvrab  47268  iccpartiun  47308  dfclnbgr6  47728  dfnbgr6  47729  uhgrimisgrgric  47783  clnbgrgrim  47786  itsclinecirc0in  48509  i0oii  48599  io1ii  48600  thincmon  48701  thincepi  48702  grptcmon  48763  grptcepi  48764