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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  eqrdav  2738  abbi1  2807  abbi2dv  2878  ss2abdv  3998  uneq1  4091  unineq  4212  difin2  4226  difsn  4732  intmin4  4909  iunconst  4934  iinconst  4935  iuneqconst  4936  dfiun2g  4961  dfiun2gOLD  4962  iindif1  5005  iindif2  5007  iinin2  5008  iunxsng  5020  iunxsngf  5022  opthprc  5652  dmopab2rex  5829  epin  6006  inimasn  6064  dmsnopg  6121  dfco2a  6154  iotaeq  6408  imadif  6525  unima  6852  ssimaex  6862  unpreima  6949  respreima  6952  iinpreima  6955  fnsnb  7047  fmptsng  7049  fmptsnd  7050  tpres  7085  iunpw  7630  ordpwsuc  7671  ordsucun  7681  fiun  7794  f1iun  7795  reldm  7894  fimaproj  7985  rntpos  8064  onoviun  8183  oarec  8402  iserd  8533  erth  8556  mapdm0  8639  mapfset  8647  ixpiin  8721  boxriin  8737  pw2f1olem  8872  fifo  9200  ordiso2  9283  ttrclse  9494  finacn  9815  acnen  9818  acacni  9905  dfac13  9907  fin23lem26  10090  isf34lem4  10142  axdc3lem2  10216  fpwwe2lem7  10402  fpwwe2lem11  10406  fpwwe2lem12  10407  gch2  10440  gchac  10446  gchina  10464  genpass  10774  1idpr  10794  eqreznegel  12683  ixxun  13104  iccid  13133  difreicc  13225  iccsplit  13226  fzsplit2  13290  fzsn  13307  fzpr  13320  uzsplit  13337  preduz  13387  predfz  13390  fz1isolem  14184  pr2pwpr  14202  isercolllem2  15386  isercoll  15388  bitsmod  16152  bitscmp  16154  saddisj  16181  sadadd  16183  sadass  16187  smupvallem  16199  smueqlem  16206  smumul  16209  gcdcllem2  16216  vdwapun  16684  firest  17152  fncnvimaeqv  17845  mhmpropd  18445  efmnd1bas  18541  subgacs  18798  eqgid  18817  ghmmhmb  18854  ghmpropd  18881  resscntz  18947  symg1bas  19007  lsmcom2  19269  lsmass  19284  ablnsg  19457  lsmcomx  19466  gsum2d2  19584  subgdmdprd  19646  dprd2d2  19656  2nsgsimpgd  19714  unitpropd  19948  subsubrg2  20060  subrgpropd  20068  rhmpropd  20069  subrgacs  20077  sdrgacs  20078  abvpropd  20111  lssacs  20238  lssats2  20271  lsspropd  20288  lmhmpropd  20344  lbspropd  20370  discld  22249  neiptopnei  22292  neiptopreu  22293  restsn  22330  restdis  22338  neitr  22340  restlp  22343  cndis  22451  cnindis  22452  cnpdis  22453  lpcls  22524  hausmapdom  22660  ptpjpre1  22731  tx1cn  22769  tx2cn  22770  hauseqlcld  22806  txkgen  22812  idqtop  22866  tgqtop  22872  acufl  23077  uffix  23081  ufildr  23091  fmfg  23109  rnelfm  23113  fmfnfm  23118  fmid  23120  fmco  23121  flimrest  23143  fclsrest  23184  alexsubALT  23211  tsmsgsum  23299  tsmssubm  23303  tsmsres  23304  tsmsf1o  23305  xpsdsval  23543  blpnf  23559  blin  23583  blres  23593  xmetec  23596  imasf1obl  23653  imasf1oxms  23654  prdsbl  23656  metrest  23689  psmetutop  23732  restmetu  23735  dscopn  23738  cnbl0  23946  bl2ioo  23964  xrtgioo  23978  cncfmet  24081  icoopnst  24111  iocopnst  24112  cldcss2  24615  iunmbl2  24730  mbfmulc2lem  24820  mbfmax  24822  ismbf3d  24827  mbfimaopnlem  24828  mbfaddlem  24833  mbfsup  24837  i1f1lem  24862  i1faddlem  24866  i1fmullem  24867  i1fmulclem  24876  i1fres  24879  mbfi1fseqlem4  24892  limcdif  25049  limcnlp  25051  limcflf  25054  limcres  25059  limcun  25068  ply1remlem  25336  fta1glem2  25340  plypf1  25382  ofmulrt  25451  plyremlem  25473  aannenlem1  25497  gausslemma2dlem1a  26522  tglineelsb2  27002  tglinecom  27005  ushgredgedg  27605  ushgredgedgloop  27607  nbumgrvtx  27722  nbusgrvtxm1uvtx  27781  vdiscusgr  27907  wspniunwspnon  28297  rusgrnumwwlkb0  28345  clwwlknscsh  28435  clwwlknun  28485  eupth2lems  28611  fusgr2wsp2nb  28707  fusgreg2wsp  28709  ubthlem1  29241  ocin  29667  shscom  29690  spansncol  29939  eqsnd  30886  iunsnima  30967  iunsnima2  30968  nfpconfp  30976  unipreima  30990  2ndimaxp  30993  suppiniseg  31029  ressupprn  31033  1stpreimas  31047  1stpreima  31048  2ndpreima  31049  fpwrelmapffslem  31076  iocinioc2  31109  nndiffz1  31116  fzsplit3  31124  swrdrn3  31236  cntzun  31329  cntzsnid  31330  ecxpid  31565  qsxpid  31567  lindspropd  31586  lsmsnpridl  31595  lsmssass  31599  grplsm0l  31600  grplsmid  31601  nsgqusf1olem2  31608  nsgqusf1olem3  31609  smatrcl  31755  qtophaus  31795  locfinreflem  31799  rspectopn  31826  zarclsiin  31830  rhmpreimacnlem  31843  prsdm  31873  prsrn  31874  indpi1  31997  indf1ofs  32003  1stmbfm  32236  2ndmbfm  32237  mbfmcnt  32244  eulerpartlemgh  32354  dstfrvunirn  32450  reprsuc  32604  reprpmtf1o  32615  satfvsucsuc  33336  dmopab3rexdif  33376  xpord2pred  33801  xpord3pred  33807  oldlim  34078  neifg  34569  filnetlem4  34579  ontgval  34629  bj-gabima  35137  bj-restsn  35262  bj-rest10  35268  bj-restpw  35272  bj-restuni  35277  mptsnunlem  35518  finxpsuclem  35577  wl-clabtv  35757  wl-clabt  35758  poimirlem16  35802  poimirlem19  35805  poimirlem23  35809  poimirlem27  35813  heicant  35821  istotbnd3  35938  sstotbnd  35942  ismtyima  35970  heibor  35988  divrngidl  36195  eccnvep  36425  ecxrn  36524  eqvrelth  36731  prtlem19  36899  prter2  36902  lkrsc  37118  lshpkr  37138  paddvaln0N  37822  paddval0  37831  diaglbN  39076  cdlemm10N  39139  lcfrvalsnN  39562  lcfrlem9  39571  lcdlss  39640  mapd1o  39669  mapd0  39686  hlhillcs  39983  sn-iotalem  40196  fnsnbt  40215  fsuppind  40286  mzpmfp  40576  lzunuz  40597  fz1eqin  40598  jm2.23  40825  pw2f1ocnv  40866  dfacbasgrp  40940  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  inintabd  41194  cnvcnvintabd  41215  cnvintabd  41218  rfcnpre3  42583  rfcnpre4  42584  rnmptpr  42720  iccshift  43063  iocopn  43065  iooshift  43067  iccintsng  43068  icoopn  43070  limcdm0  43166  limcresiooub  43190  limcresioolb  43191  fperdvper  43467  itgperiod  43529  fourierdlem32  43687  fourierdlem33  43688  fourierdlem48  43702  fourierdlem49  43703  fourierdlem81  43735  fsetsniunop  44554  elsetpreimafvrab  44857  iccpartiun  44897  mgmhmpropd  45350  rnghmval2  45464  itsclinecirc0in  46132  i0oii  46224  io1ii  46225  thincmon  46326  thincepi  46327  grptcmon  46388  grptcepi  46389