Theorem eqrdv 2763

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

Syntax hints:   → wi 4   ↔ wb 197  ∀wal 1650   = wceq 1652   ∈ wcel 2155

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758

This theorem is referenced by:  eqrdav  2764  uneq1  3922  ineq1  3969  unineq  4042  difin2  4054  difsn  4483  intmin4  4662  iunconst  4685  iinconst  4686  dfiun2g  4708  iindif2  4745  iinin2  4746  iunxsng  4758  iunxsngf  4760  opthprc  5335  inimasn  5733  dmsnopg  5790  dfco2a  5821  iotaeq  6039  imadif  6151  ssimaex  6452  unpreima  6531  respreima  6534  iinpreima  6535  fnsnb  6625  fmptsng  6627  fmptsnd  6628  tpres  6659  iunpw  7176  ordpwsuc  7213  ordsucun  7223  fun11iun  7324  reldm  7419  rntpos  7568  onoviun  7644  oarec  7847  iserd  7973  erth  7994  mapdm0  8075  map0eOLD  8099  ixpiin  8139  boxriin  8155  pw2f1olem  8271  fifo  8545  ordiso2  8627  finacn  9124  acnen  9127  acacni  9215  dfac13  9217  fin23lem26  9400  isf34lem4  9452  axdc3lem2  9526  fpwwe2lem8  9712  fpwwe2lem12  9716  fpwwe2lem13  9717  gch2  9750  gchac  9756  gchina  9774  genpass  10084  1idpr  10104  eqreznegel  11975  ixxun  12393  iccid  12422  difreicc  12511  iccsplit  12512  fzsplit2  12573  fzsn  12590  fzpr  12603  uzsplit  12619  preduz  12669  predfz  12672  fz1isolem  13446  pr2pwpr  13462  isercolllem2  14683  isercoll  14685  bitsmod  15441  bitscmp  15443  saddisj  15470  sadadd  15472  sadass  15476  smupvallem  15488  smueqlem  15495  smumul  15498  gcdcllem2  15505  vdwapun  15959  firest  16361  fncnvimaeqv  17027  mhmpropd  17609  subgacs  17895  eqgid  17912  ghmmhmb  17937  ghmpropd  17964  resscntz  18029  symg1bas  18081  lsmcom2  18336  lsmass  18349  ablnsg  18516  lsmcomx  18525  gsum2d2  18639  subgdmdprd  18700  dprd2d2  18710  unitpropd  18964  subsubrg2  19076  subrgpropd  19083  rhmpropd  19084  abvpropd  19111  lssacs  19239  lssats2  19272  lsspropd  19289  lmhmpropd  19345  lbspropd  19371  discld  21173  neiptopnei  21216  neiptopreu  21217  restsn  21254  restdis  21262  neitr  21264  restlp  21267  cndis  21375  cnindis  21376  cnpdis  21377  lpcls  21448  hausmapdom  21583  ptpjpre1  21654  tx1cn  21692  tx2cn  21693  hauseqlcld  21729  txkgen  21735  idqtop  21789  tgqtop  21795  acufl  22000  uffix  22004  ufildr  22014  fmfg  22032  rnelfm  22036  fmfnfm  22041  fmid  22043  fmco  22044  flimrest  22066  fclsrest  22107  alexsubALT  22134  tsmsgsum  22221  tsmssubm  22225  tsmsres  22226  tsmsf1o  22227  xpsdsval  22465  blpnf  22481  blin  22505  blres  22515  xmetec  22518  imasf1obl  22572  imasf1oxms  22573  prdsbl  22575  metrest  22608  psmetutop  22651  restmetu  22654  dscopn  22657  cnbl0  22856  bl2ioo  22874  xrtgioo  22888  cncfmet  22990  icoopnst  23017  iocopnst  23018  cldcss2  23502  iunmbl2  23615  mbfmulc2lem  23705  mbfmax  23707  ismbf3d  23712  mbfimaopnlem  23713  mbfaddlem  23718  mbfsup  23722  i1f1lem  23747  i1faddlem  23751  i1fmullem  23752  i1fmulclem  23760  i1fres  23763  mbfi1fseqlem4  23776  limcdif  23931  limcnlp  23933  limcflf  23936  limcres  23941  limcun  23950  ply1remlem  24213  fta1glem2  24217  plypf1  24259  ofmulrt  24328  plyremlem  24350  aannenlem1  24374  gausslemma2dlem1a  25381  tglineelsb2  25818  tglinecom  25821  ushgredgedg  26399  ushgredgedgloop  26401  ushgredgedgloopOLD  26402  nbumgrvtx  26521  nbusgrvtxm1uvtx  26591  vdiscusgr  26718  wspniunwspnon  27126  rusgrnumwwlkb0  27176  clwwlknscsh  27276  clwwlknun  27344  clwwlknunOLD  27349  eupth2lems  27474  fusgr2wsp2nb  27572  fusgreg2wsp  27574  ubthlem1  28117  ocin  28546  shscom  28569  spansncol  28818  iunsnima  29813  unipreima  29831  1stpreimas  29867  1stpreima  29868  2ndpreima  29869  fpwrelmapffslem  29891  iocinioc2  29925  nndiffz1  29932  fzsplit3  29937  smatrcl  30244  fimaproj  30282  qtophaus  30285  locfinreflem  30289  prsdm  30342  prsrn  30343  indpi1  30464  indf1ofs  30470  1stmbfm  30704  2ndmbfm  30705  mbfmcnt  30712  eulerpartlemgh  30822  dstfrvunirn  30919  reprsuc  31076  reprpmtf1o  31087  neifg  32741  filnetlem4  32751  ontgval  32801  bj-restsn  33395  bj-rest10  33401  bj-restpw  33405  bj-restuni  33410  mptsnunlem  33551  finxpsuclem  33599  poimirlem16  33781  poimirlem19  33784  poimirlem23  33788  poimirlem27  33792  heicant  33800  istotbnd3  33924  sstotbnd  33928  ismtyima  33956  heibor  33974  divrngidl  34181  eccnvep  34411  ecxrn  34510  eqvrelth  34714  prtlem19  34766  prter2  34769  lkrsc  34985  lshpkr  35005  paddvaln0N  35689  paddval0  35698  diaglbN  36943  cdlemm10N  37006  lcfrvalsnN  37429  lcfrlem9  37438  lcdlss  37507  mapd1o  37536  mapd0  37553  hlhillcs  37846  mzpmfp  37920  lzunuz  37941  fz1eqin  37942  jm2.23  38172  pw2f1ocnv  38213  dfacbasgrp  38287  subrgacs  38379  sdrgacs  38380  inintabd  38492  cnvcnvintabd  38513  cnvintabd  38516  rfcnpre3  39776  rfcnpre4  39777  iunxsngf2  39813  unima  39925  iccshift  40315  iocopn  40317  iooshift  40319  iccintsng  40320  icoopn  40322  limcdm0  40420  limcresiooub  40444  limcresioolb  40445  fperdvper  40703  itgperiod  40766  fourierdlem32  40925  fourierdlem33  40926  fourierdlem48  40940  fourierdlem49  40941  fourierdlem81  40973  iccpartiun  42036  mgmhmpropd  42386  rnghmval2  42496