Theorem eqrdv 2733

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  eqrdav  2734  abbi  2800  eqabdv  2868  uneq1  4136  unineq  4263  difin2  4276  difsn  4774  eqsndOLD  4807  intmin4  4953  iunconst  4977  iinconst  4978  iuneqconst  4979  dfiun2g  5006  dfiun2gOLD  5007  iindif1  5051  iindif2  5053  iinin2  5054  iunxsng  5066  iunxsngf  5068  opthprc  5718  dmopab2rex  5897  dmxp  5908  epin  6082  inimasn  6145  dmsnopg  6202  dfco2a  6235  iotaeq  6496  imadif  6620  unima  6954  ssimaex  6964  unpreima  7053  respreima  7056  iinpreima  7059  fnsnbg  7156  fnsnbOLD  7158  fmptsng  7160  fmptsnd  7161  tpres  7193  iunpw  7765  ordpwsuc  7809  ordsucun  7819  fiun  7941  f1iun  7942  reldm  8043  fimaproj  8134  xpord2pred  8144  xpord3pred  8151  rntpos  8238  onoviun  8357  oarec  8574  iserd  8745  erth  8770  mapdm0  8856  mapfset  8864  ixpiin  8938  boxriin  8954  pw2f1olem  9090  fifo  9444  ordiso2  9529  ttrclse  9741  finacn  10064  acnen  10067  acacni  10155  dfac13  10157  fin23lem26  10339  isf34lem4  10391  axdc3lem2  10465  fpwwe2lem7  10651  fpwwe2lem11  10655  fpwwe2lem12  10656  gch2  10689  gchac  10695  gchina  10713  genpass  11023  1idpr  11043  eqreznegel  12950  ixxun  13378  iccid  13407  difreicc  13501  iccsplit  13502  fzsplit2  13566  fzsn  13583  fzpr  13596  uzsplit  13613  fzdif1  13622  preduz  13667  predfz  13670  fz1isolem  14479  pr2pwpr  14497  isercolllem2  15682  isercoll  15684  bitsmod  16455  bitscmp  16457  saddisj  16484  sadadd  16486  sadass  16490  smupvallem  16502  smueqlem  16509  smumul  16512  gcdcllem2  16519  vdwapun  16994  firest  17446  fncnvimaeqv  18132  mgmhmpropd  18676  mhmpropd  18770  efmnd1bas  18871  subgacs  19144  eqgid  19163  ghmmhmb  19210  ghmpropd  19239  ghmqusnsglem1  19263  ghmquskerlem1  19266  ghmqusker  19270  resscntz  19316  symg1bas  19372  lsmcom2  19636  lsmass  19650  ablnsg  19828  lsmcomx  19837  gsum2d2  19955  subgdmdprd  20017  dprd2d2  20027  2nsgsimpgd  20085  unitpropd  20377  rnghmval2  20404  subsubrng2  20524  subrngpropd  20528  subsubrg2  20559  subrgpropd  20568  rhmpropd  20569  subrgacs  20760  sdrgacs  20761  abvpropd  20795  lssacs  20924  lssats2  20957  lsspropd  20975  lmhmpropd  21031  lbspropd  21057  pzriprnglem10  21451  psdmul  22104  discld  23027  neiptopnei  23070  neiptopreu  23071  restsn  23108  restdis  23116  neitr  23118  restlp  23121  cndis  23229  cnindis  23230  cnpdis  23231  lpcls  23302  hausmapdom  23438  ptpjpre1  23509  tx1cn  23547  tx2cn  23548  hauseqlcld  23584  txkgen  23590  idqtop  23644  tgqtop  23650  acufl  23855  uffix  23859  ufildr  23869  fmfg  23887  rnelfm  23891  fmfnfm  23896  fmid  23898  fmco  23899  flimrest  23921  fclsrest  23962  alexsubALT  23989  tsmsgsum  24077  tsmssubm  24081  tsmsres  24082  tsmsf1o  24083  xpsdsval  24320  blpnf  24336  blin  24360  blres  24370  xmetec  24373  imasf1obl  24427  imasf1oxms  24428  prdsbl  24430  metrest  24463  psmetutop  24506  restmetu  24509  dscopn  24512  cnbl0  24712  bl2ioo  24731  xrtgioo  24746  cncfmet  24853  icoopnst  24887  iocopnst  24888  cldcss2  25394  iunmbl2  25510  mbfmulc2lem  25600  mbfmax  25602  ismbf3d  25607  mbfimaopnlem  25608  mbfaddlem  25613  mbfsup  25617  i1f1lem  25642  i1faddlem  25646  i1fmullem  25647  i1fmulclem  25655  i1fres  25658  mbfi1fseqlem4  25671  limcdif  25829  limcnlp  25831  limcflf  25834  limcres  25839  limcun  25848  ply1remlem  26122  fta1glem2  26126  plypf1  26169  ofmulrt  26241  plyremlem  26264  aannenlem1  26288  gausslemma2dlem1a  27328  oldlim  27850  tglineelsb2  28611  tglinecom  28614  ushgredgedg  29208  ushgredgedgloop  29210  nbumgrvtx  29325  nbusgrvtxm1uvtx  29384  vdiscusgr  29511  wspniunwspnon  29905  rusgrnumwwlkb0  29953  clwwlknscsh  30043  clwwlknun  30093  eupth2lems  30219  fusgr2wsp2nb  30315  fusgreg2wsp  30317  ubthlem1  30851  ocin  31277  shscom  31300  spansncol  31549  iunsnima  32598  iunsnima2  32599  nfpconfp  32610  unipreima  32621  2ndimaxp  32624  fdifsupp  32662  suppiniseg  32663  ressupprn  32667  1stpreimas  32683  1stpreima  32684  2ndpreima  32685  fpwrelmapffslem  32709  iocinioc2  32756  nndiffz1  32763  fzsplit3  32770  indpi1  32837  indf1ofs  32843  swrdrn3  32931  cntzun  33062  cntzsnid  33063  ecxpid  33376  qsxpid  33377  lindspropd  33398  lsmsnpridl  33413  lsmssass  33417  grplsm0l  33418  grplsmid  33419  nsgqusf1olem2  33429  nsgqusf1olem3  33430  crngmxidl  33484  opprlidlabs  33500  rprmirredb  33547  ressply1mon1p  33581  fldextrspunlsp  33715  irngnzply1  33732  smatrcl  33827  qtophaus  33867  locfinreflem  33871  rspectopn  33898  zarclsiin  33902  rhmpreimacnlem  33915  prsdm  33945  prsrn  33946  1stmbfm  34292  2ndmbfm  34293  mbfmcnt  34300  eulerpartlemgh  34410  dstfrvunirn  34507  reprsuc  34647  reprpmtf1o  34658  satfvsucsuc  35387  dmopab3rexdif  35427  cbvabdavw  36274  neifg  36389  filnetlem4  36399  ontgval  36449  bj-gabima  36958  bj-restsn  37100  bj-rest10  37106  bj-restpw  37110  bj-restuni  37115  mptsnunlem  37356  finxpsuclem  37415  wl-clabtv  37615  wl-clabt  37616  poimirlem16  37660  poimirlem19  37663  poimirlem23  37667  poimirlem27  37671  heicant  37679  istotbnd3  37795  sstotbnd  37799  ismtyima  37827  heibor  37845  divrngidl  38052  eccnvep  38300  ecxrn  38405  eqvrelth  38629  disjlem19  38819  prtlem19  38896  prter2  38899  lkrsc  39115  lshpkr  39135  paddvaln0N  39820  paddval0  39829  diaglbN  41074  cdlemm10N  41137  lcfrvalsnN  41560  lcfrlem9  41569  lcdlss  41638  mapd1o  41667  mapd0  41684  hlhillcs  41977  grpods  42207  unitscyglem2  42209  sn-iotalem  42272  fsuppind  42613  mzpmfp  42770  lzunuz  42791  fz1eqin  42792  jm2.23  43020  pw2f1ocnv  43061  dfacbasgrp  43132  nnoeomeqom  43336  oadif1lem  43403  oadif1  43404  fzunt  43479  fzuntd  43480  fzunt1d  43481  fzuntgd  43482  inintabd  43603  cnvcnvintabd  43624  cnvintabd  43627  rfcnpre3  45057  rfcnpre4  45058  iindif2f  45184  rnmptpr  45201  iccshift  45547  iocopn  45549  iooshift  45551  iccintsng  45552  icoopn  45554  limcdm0  45647  limcresiooub  45671  limcresioolb  45672  fperdvper  45948  itgperiod  46010  fourierdlem32  46168  fourierdlem33  46169  fourierdlem48  46183  fourierdlem49  46184  fourierdlem81  46216  fsetsniunop  47078  elsetpreimafvrab  47408  iccpartiun  47448  dfclnbgr6  47869  dfnbgr6  47870  uhgrimisgrgric  47944  clnbgrgrim  47947  stgredgiun  47970  gpgnbgrvtx0  48076  gpgnbgrvtx1  48077  itsclinecirc0in  48755  i0oii  48894  io1ii  48895  sectpropd  49004  invpropd  49006  isopropd  49008  cicpropd  49017  thincmon  49319  thincepi  49320  grptcmon  49470  grptcepi  49471  lanval2  49502  ranval2  49505