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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1541   = wceq 1543   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2729

This theorem is referenced by:  eqrdav  2736  abbi1  2806  abbi2dv  2874  ss2abdv  3977  uneq1  4070  unineq  4192  difin2  4206  difsn  4711  intmin4  4888  iunconst  4913  iinconst  4914  iuneqconst  4915  dfiun2g  4940  iindif1  4983  iindif2  4985  iinin2  4986  iunxsng  4998  iunxsngf  5000  opthprc  5613  dmopab2rex  5786  epin  5963  inimasn  6019  dmsnopg  6076  dfco2a  6110  iotaeq  6351  imadif  6464  unima  6786  ssimaex  6796  unpreima  6883  respreima  6886  iinpreima  6889  fnsnb  6981  fmptsng  6983  fmptsnd  6984  tpres  7016  iunpw  7556  ordpwsuc  7594  ordsucun  7604  fiun  7716  f1iun  7717  reldm  7815  fimaproj  7902  rntpos  7981  onoviun  8080  oarec  8290  iserd  8417  erth  8440  mapdm0  8523  mapfset  8531  ixpiin  8605  boxriin  8621  pw2f1olem  8749  fifo  9048  ordiso2  9131  finacn  9664  acnen  9667  acacni  9754  dfac13  9756  fin23lem26  9939  isf34lem4  9991  axdc3lem2  10065  fpwwe2lem7  10251  fpwwe2lem11  10255  fpwwe2lem12  10256  gch2  10289  gchac  10295  gchina  10313  genpass  10623  1idpr  10643  eqreznegel  12530  ixxun  12951  iccid  12980  difreicc  13072  iccsplit  13073  fzsplit2  13137  fzsn  13154  fzpr  13167  uzsplit  13184  preduz  13234  predfz  13237  fz1isolem  14027  pr2pwpr  14045  isercolllem2  15229  isercoll  15231  bitsmod  15995  bitscmp  15997  saddisj  16024  sadadd  16026  sadass  16030  smupvallem  16042  smueqlem  16049  smumul  16052  gcdcllem2  16059  vdwapun  16527  firest  16937  fncnvimaeqv  17627  mhmpropd  18224  efmnd1bas  18320  subgacs  18577  eqgid  18596  ghmmhmb  18633  ghmpropd  18660  resscntz  18726  symg1bas  18783  lsmcom2  19044  lsmass  19059  ablnsg  19232  lsmcomx  19241  gsum2d2  19359  subgdmdprd  19421  dprd2d2  19431  2nsgsimpgd  19489  unitpropd  19715  subsubrg2  19827  subrgpropd  19835  rhmpropd  19836  subrgacs  19844  sdrgacs  19845  abvpropd  19878  lssacs  20004  lssats2  20037  lsspropd  20054  lmhmpropd  20110  lbspropd  20136  discld  21986  neiptopnei  22029  neiptopreu  22030  restsn  22067  restdis  22075  neitr  22077  restlp  22080  cndis  22188  cnindis  22189  cnpdis  22190  lpcls  22261  hausmapdom  22397  ptpjpre1  22468  tx1cn  22506  tx2cn  22507  hauseqlcld  22543  txkgen  22549  idqtop  22603  tgqtop  22609  acufl  22814  uffix  22818  ufildr  22828  fmfg  22846  rnelfm  22850  fmfnfm  22855  fmid  22857  fmco  22858  flimrest  22880  fclsrest  22921  alexsubALT  22948  tsmsgsum  23036  tsmssubm  23040  tsmsres  23041  tsmsf1o  23042  xpsdsval  23279  blpnf  23295  blin  23319  blres  23329  xmetec  23332  imasf1obl  23386  imasf1oxms  23387  prdsbl  23389  metrest  23422  psmetutop  23465  restmetu  23468  dscopn  23471  cnbl0  23671  bl2ioo  23689  xrtgioo  23703  cncfmet  23806  icoopnst  23836  iocopnst  23837  cldcss2  24339  iunmbl2  24454  mbfmulc2lem  24544  mbfmax  24546  ismbf3d  24551  mbfimaopnlem  24552  mbfaddlem  24557  mbfsup  24561  i1f1lem  24586  i1faddlem  24590  i1fmullem  24591  i1fmulclem  24600  i1fres  24603  mbfi1fseqlem4  24616  limcdif  24773  limcnlp  24775  limcflf  24778  limcres  24783  limcun  24792  ply1remlem  25060  fta1glem2  25064  plypf1  25106  ofmulrt  25175  plyremlem  25197  aannenlem1  25221  gausslemma2dlem1a  26246  tglineelsb2  26723  tglinecom  26726  ushgredgedg  27317  ushgredgedgloop  27319  nbumgrvtx  27434  nbusgrvtxm1uvtx  27493  vdiscusgr  27619  wspniunwspnon  28007  rusgrnumwwlkb0  28055  clwwlknscsh  28145  clwwlknun  28195  eupth2lems  28321  fusgr2wsp2nb  28417  fusgreg2wsp  28419  ubthlem1  28951  ocin  29377  shscom  29400  spansncol  29649  eqsnd  30596  iunsnima  30677  iunsnima2  30678  nfpconfp  30686  unipreima  30700  2ndimaxp  30703  suppiniseg  30740  ressupprn  30744  1stpreimas  30758  1stpreima  30759  2ndpreima  30760  fpwrelmapffslem  30787  iocinioc2  30820  nndiffz1  30827  fzsplit3  30835  swrdrn3  30947  cntzun  31039  cntzsnid  31040  ecxpid  31270  qsxpid  31272  lindspropd  31291  lsmsnpridl  31300  lsmssass  31304  grplsm0l  31305  grplsmid  31306  nsgqusf1olem2  31313  nsgqusf1olem3  31314  smatrcl  31460  qtophaus  31500  locfinreflem  31504  rspectopn  31531  zarclsiin  31535  rhmpreimacnlem  31548  prsdm  31578  prsrn  31579  indpi1  31700  indf1ofs  31706  1stmbfm  31939  2ndmbfm  31940  mbfmcnt  31947  eulerpartlemgh  32057  dstfrvunirn  32153  reprsuc  32307  reprpmtf1o  32318  satfvsucsuc  33040  dmopab3rexdif  33080  xpord2pred  33529  xpord3pred  33535  oldlim  33806  neifg  34297  filnetlem4  34307  ontgval  34357  bj-gabima  34865  bj-restsn  34988  bj-rest10  34994  bj-restpw  34998  bj-restuni  35003  mptsnunlem  35246  finxpsuclem  35305  wl-clabtv  35485  wl-clabt  35486  poimirlem16  35530  poimirlem19  35533  poimirlem23  35537  poimirlem27  35541  heicant  35549  istotbnd3  35666  sstotbnd  35670  ismtyima  35698  heibor  35716  divrngidl  35923  eccnvep  36154  ecxrn  36254  eqvrelth  36461  prtlem19  36629  prter2  36632  lkrsc  36848  lshpkr  36868  paddvaln0N  37552  paddval0  37561  diaglbN  38806  cdlemm10N  38869  lcfrvalsnN  39292  lcfrlem9  39301  lcdlss  39370  mapd1o  39399  mapd0  39416  hlhillcs  39709  fnsnbt  39921  fsuppind  39989  mzpmfp  40272  lzunuz  40293  fz1eqin  40294  jm2.23  40521  pw2f1ocnv  40562  dfacbasgrp  40636  inintabd  40863  cnvcnvintabd  40884  cnvintabd  40887  rfcnpre3  42249  rfcnpre4  42250  rnmptpr  42386  iccshift  42731  iocopn  42733  iooshift  42735  iccintsng  42736  icoopn  42738  limcdm0  42834  limcresiooub  42858  limcresioolb  42859  fperdvper  43135  itgperiod  43197  fourierdlem32  43355  fourierdlem33  43356  fourierdlem48  43370  fourierdlem49  43371  fourierdlem81  43403  fsetsniunop  44215  elsetpreimafvrab  44519  iccpartiun  44559  mgmhmpropd  45012  rnghmval2  45126  itsclinecirc0in  45794  i0oii  45886  io1ii  45887  thincmon  45988  thincepi  45989  grptcmon  46048  grptcepi  46049