Theorem eqrdv 2796

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   = wceq 1538   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  eqrdav  2797  abbi1  2861  abbi2dv  2927  ss2abdv  3991  uneq1  4083  ineq1OLD  4132  unineq  4204  difin2  4216  difsn  4691  intmin4  4867  iunconst  4890  iinconst  4891  iuneqconst  4892  dfiun2g  4917  dfiun2gOLD  4918  iindif1  4960  iindif2  4962  iinin2  4963  iunxsng  4975  iunxsngf  4977  opthprc  5580  dmopab2rex  5750  inimasn  5980  dmsnopg  6037  dfco2a  6066  iotaeq  6295  imadif  6408  unima  6714  ssimaex  6723  unpreima  6810  respreima  6813  iinpreima  6814  fnsnb  6905  fmptsng  6907  fmptsnd  6908  tpres  6940  iunpw  7473  ordpwsuc  7510  ordsucun  7520  fiun  7626  f1iun  7627  reldm  7725  fimaproj  7812  rntpos  7888  onoviun  7963  oarec  8171  iserd  8298  erth  8321  mapdm0  8404  ixpiin  8471  boxriin  8487  pw2f1olem  8604  fifo  8880  ordiso2  8963  finacn  9461  acnen  9464  acacni  9551  dfac13  9553  fin23lem26  9736  isf34lem4  9788  axdc3lem2  9862  fpwwe2lem8  10048  fpwwe2lem12  10052  fpwwe2lem13  10053  gch2  10086  gchac  10092  gchina  10110  genpass  10420  1idpr  10440  eqreznegel  12322  ixxun  12742  iccid  12771  difreicc  12862  iccsplit  12863  fzsplit2  12927  fzsn  12944  fzpr  12957  uzsplit  12974  preduz  13024  predfz  13027  fz1isolem  13815  pr2pwpr  13833  isercolllem2  15014  isercoll  15016  bitsmod  15775  bitscmp  15777  saddisj  15804  sadadd  15806  sadass  15810  smupvallem  15822  smueqlem  15829  smumul  15832  gcdcllem2  15839  vdwapun  16300  firest  16698  fncnvimaeqv  17362  mhmpropd  17954  efmnd1bas  18050  subgacs  18305  eqgid  18324  ghmmhmb  18361  ghmpropd  18388  resscntz  18454  symg1bas  18511  lsmcom2  18772  lsmass  18787  ablnsg  18960  lsmcomx  18969  gsum2d2  19087  subgdmdprd  19149  dprd2d2  19159  2nsgsimpgd  19217  unitpropd  19443  subsubrg2  19555  subrgpropd  19563  rhmpropd  19564  subrgacs  19572  sdrgacs  19573  abvpropd  19606  lssacs  19732  lssats2  19765  lsspropd  19782  lmhmpropd  19838  lbspropd  19864  discld  21694  neiptopnei  21737  neiptopreu  21738  restsn  21775  restdis  21783  neitr  21785  restlp  21788  cndis  21896  cnindis  21897  cnpdis  21898  lpcls  21969  hausmapdom  22105  ptpjpre1  22176  tx1cn  22214  tx2cn  22215  hauseqlcld  22251  txkgen  22257  idqtop  22311  tgqtop  22317  acufl  22522  uffix  22526  ufildr  22536  fmfg  22554  rnelfm  22558  fmfnfm  22563  fmid  22565  fmco  22566  flimrest  22588  fclsrest  22629  alexsubALT  22656  tsmsgsum  22744  tsmssubm  22748  tsmsres  22749  tsmsf1o  22750  xpsdsval  22988  blpnf  23004  blin  23028  blres  23038  xmetec  23041  imasf1obl  23095  imasf1oxms  23096  prdsbl  23098  metrest  23131  psmetutop  23174  restmetu  23177  dscopn  23180  cnbl0  23379  bl2ioo  23397  xrtgioo  23411  cncfmet  23514  icoopnst  23544  iocopnst  23545  cldcss2  24046  iunmbl2  24161  mbfmulc2lem  24251  mbfmax  24253  ismbf3d  24258  mbfimaopnlem  24259  mbfaddlem  24264  mbfsup  24268  i1f1lem  24293  i1faddlem  24297  i1fmullem  24298  i1fmulclem  24306  i1fres  24309  mbfi1fseqlem4  24322  limcdif  24479  limcnlp  24481  limcflf  24484  limcres  24489  limcun  24498  ply1remlem  24763  fta1glem2  24767  plypf1  24809  ofmulrt  24878  plyremlem  24900  aannenlem1  24924  gausslemma2dlem1a  25949  tglineelsb2  26426  tglinecom  26429  ushgredgedg  27019  ushgredgedgloop  27021  nbumgrvtx  27136  nbusgrvtxm1uvtx  27195  vdiscusgr  27321  wspniunwspnon  27709  rusgrnumwwlkb0  27757  clwwlknscsh  27847  clwwlknun  27897  eupth2lems  28023  fusgr2wsp2nb  28119  fusgreg2wsp  28121  ubthlem1  28653  ocin  29079  shscom  29102  spansncol  29351  eqsnd  30301  iunsnima  30382  iunsnima2  30383  nfpconfp  30391  unipreima  30405  2ndimaxp  30409  suppiniseg  30446  ressupprn  30450  1stpreimas  30465  1stpreima  30466  2ndpreima  30467  fpwrelmapffslem  30494  iocinioc2  30528  nndiffz1  30535  fzsplit3  30543  swrdrn3  30655  cntzun  30745  cntzsnid  30746  ecxpid  30976  qsxpid  30978  lindspropd  30997  lsmsnpridl  31005  lsmssass  31009  smatrcl  31149  qtophaus  31189  locfinreflem  31193  rspectopn  31220  zarclsiin  31224  rhmpreimacnlem  31237  prsdm  31267  prsrn  31268  indpi1  31389  indf1ofs  31395  1stmbfm  31628  2ndmbfm  31629  mbfmcnt  31636  eulerpartlemgh  31746  dstfrvunirn  31842  reprsuc  31996  reprpmtf1o  32007  satfvsucsuc  32725  dmopab3rexdif  32765  neifg  33832  filnetlem4  33842  ontgval  33892  bj-restsn  34497  bj-rest10  34503  bj-restpw  34507  bj-restuni  34512  mptsnunlem  34755  finxpsuclem  34814  wl-clabtv  34994  wl-clabt  34995  wl-dfrabf  35029  poimirlem16  35073  poimirlem19  35076  poimirlem23  35080  poimirlem27  35084  heicant  35092  istotbnd3  35209  sstotbnd  35213  ismtyima  35241  heibor  35259  divrngidl  35466  eccnvep  35699  ecxrn  35799  eqvrelth  36006  prtlem19  36174  prter2  36177  lkrsc  36393  lshpkr  36413  paddvaln0N  37097  paddval0  37106  diaglbN  38351  cdlemm10N  38414  lcfrvalsnN  38837  lcfrlem9  38846  lcdlss  38915  mapd1o  38944  mapd0  38961  hlhillcs  39254  fnsnbt  39414  fsuppind  39456  mzpmfp  39688  lzunuz  39709  fz1eqin  39710  jm2.23  39937  pw2f1ocnv  39978  dfacbasgrp  40052  inintabd  40279  cnvcnvintabd  40300  cnvintabd  40303  rfcnpre3  41662  rfcnpre4  41663  rnmptpr  41801  iccshift  42155  iocopn  42157  iooshift  42159  iccintsng  42160  icoopn  42162  limcdm0  42260  limcresiooub  42284  limcresioolb  42285  fperdvper  42561  itgperiod  42623  fourierdlem32  42781  fourierdlem33  42782  fourierdlem48  42796  fourierdlem49  42797  fourierdlem81  42829  elsetpreimafvrab  43911  iccpartiun  43951  mgmhmpropd  44405  rnghmval2  44519  itsclinecirc0in  45189