Theorem eqrdv 2767

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  eqrdav  2768  abbi  2834  eqabdv  2902  uneq1  4123  unineq  4249  difin2  4262  difsn  4767  intmin4  4943  intprg  4947  iunconst  4967  iinconst  4968  iuneqconst  4969  dfiun2g  4995  iindif1  5042  iindif2  5044  iinin2  5045  iunxsng  5057  iunxsngf  5059  opthprc  5723  dmopab2rex  5905  dmxp  5917  epin  6095  inimasn  6151  dmsnopg  6212  dfco2a  6245  iotaeq  6502  imadif  6618  unima  6954  ssimaex  6964  unpreima  7056  respreima  7059  iinpreima  7062  fnsnbg  7160  fnsnbOLD  7162  fmptsng  7164  fmptsnd  7165  tpres  7197  iunpw  7766  ordpwsuc  7807  ordsucun  7817  fiun  7936  f1iun  7937  reldm  8037  fimaproj  8127  xpord2pred  8137  xpord3pred  8144  rntpos  8231  onoviun  8326  oarec  8543  iserd  8717  erth  8745  mapdm0  8835  mapfset  8843  ixpiin  8918  boxriin  8934  pw2f1olem  9065  fifo  9388  ordiso2  9473  ttrclse  9692  finacn  10030  acnen  10033  acacni  10120  dfac13  10122  fin23lem26  10305  isf34lem4  10357  axdc3lem2  10431  fpwwe2lem7  10618  fpwwe2lem11  10622  fpwwe2lem12  10623  gch2  10656  gchac  10662  gchina  10680  genpass  10990  1idpr  11010  indpi1  12228  eqreznegel  12954  ixxun  13384  iccid  13413  difreicc  13507  iccsplit  13508  fzsplit2  13573  fzsn  13590  fzpr  13603  uzsplit  13620  fzdif1  13629  preduz  13674  predfz  13677  fz1isolem  14494  pr2pwpr  14512  isercolllem2  15713  isercoll  15715  bitsmod  16490  bitscmp  16492  saddisj  16519  sadadd  16521  sadass  16525  smupvallem  16537  smueqlem  16544  smumul  16547  gcdcllem2  16554  vdwapun  17030  firest  17481  fncnvimaeqv  18172  mgmhmpropd  18752  mhmpropd  18846  efmnd1bas  18948  subgacs  19223  ecxpid  19238  qsxpid  19239  eqgid  19244  ghmmhmb  19293  ghmpropd  19322  ghmqusnsglem1  19346  ghmquskerlem1  19349  ghmqusker  19353  resscntz  19399  symg1bas  19457  lsmcom2  19721  lsmass  19735  ablnsg  19913  lsmcomx  19922  gsum2d2  20040  subgdmdprd  20102  dprd2d2  20112  2nsgsimpgd  20170  unitpropd  20495  rnghmval2  20522  subsubrng2  20645  subrngpropd  20649  subsubrg2  20680  subrgpropd  20689  rhmpropd  20690  subrgacs  20877  sdrgacs  20878  abvpropd  20912  lssacs  21062  lssats2  21095  lsspropd  21112  lmhmpropd  21168  lbspropd  21194  pzriprnglem10  21605  psdmul  22294  discld  23211  neiptopnei  23254  neiptopreu  23255  restsn  23292  restdis  23300  neitr  23302  restlp  23305  cndis  23413  cnindis  23414  cnpdis  23415  lpcls  23486  hausmapdom  23622  ptpjpre1  23693  tx1cn  23731  tx2cn  23732  hauseqlcld  23768  txkgen  23774  idqtop  23828  tgqtop  23834  acufl  24039  uffix  24043  ufildr  24053  fmfg  24071  rnelfm  24075  fmfnfm  24080  fmid  24082  fmco  24083  flimrest  24105  fclsrest  24146  alexsubALT  24173  tsmsgsum  24261  tsmssubm  24265  tsmsres  24266  tsmsf1o  24267  xpsdsval  24503  blpnf  24519  blin  24543  blres  24553  xmetec  24556  imasf1obl  24610  imasf1oxms  24611  prdsbl  24613  metrest  24646  psmetutop  24689  restmetu  24692  dscopn  24695  cnbl0  24895  bl2ioo  24914  xrtgioo  24929  cncfmet  25033  icoopnst  25063  iocopnst  25064  cldcss2  25566  iunmbl2  25681  mbfmulc2lem  25771  mbfmax  25773  ismbf3d  25778  mbfimaopnlem  25779  mbfaddlem  25784  mbfsup  25788  i1f1lem  25813  i1faddlem  25817  i1fmullem  25818  i1fmulclem  25826  i1fres  25829  mbfi1fseqlem4  25842  limcdif  26000  limcnlp  26002  limcflf  26005  limcres  26010  limcun  26019  ply1remlem  26287  fta1glem2  26291  plypf1  26334  ofmulrt  26405  plyremlem  26430  aannenlem1  26454  gausslemma2dlem1a  27491  oldlim  28042  negleft  28213  negright  28214  tglineelsb2  28863  tglinecom  28866  ushgredgedg  29516  ushgredgedgloop  29518  nbumgrvtx  29633  nbusgrvtxm1uvtx  29692  vdiscusgr  29818  wspniunwspnon  30209  rusgrnumwwlkb0  30260  clwwlknscsh  30350  clwwlknun  30400  eupth2lems  30526  fusgr2wsp2nb  30622  fusgreg2wsp  30624  ubthlem1  31159  ocin  31585  shscom  31608  spansncol  31857  iunsnima  32900  iunsnima2  32901  nfpconfp  32914  unipreima  32925  2ndimaxp  32928  fdifsupp  32967  suppiniseg  32968  ressupprn  32972  1stpreimas  32988  1stpreima  32989  2ndpreima  32990  fpwrelmapffslem  33014  iocinioc2  33061  nndiffz1  33068  fzsplit3  33075  indf1ofs  33123  swrdrn3  33212  cntzun  33336  cntzsnid  33337  cntrval2  33428  lindspropd  33636  lsmsnpridl  33649  lsmssass  33651  grplsm0l  33652  grplsmid  33653  nsgqusf1olem2  33663  nsgqusf1olem3  33664  crngmxidl  33693  opprlidlabs  33708  rprmirredb  33763  ressply1mon1p  33799  fldextrspunlsp  34005  irngnzply1  34022  smatrcl  34127  qtophaus  34167  locfinreflem  34171  rspectopn  34198  zarclsiin  34202  rhmpreimacnlem  34215  prsdm  34245  prsrn  34246  1stmbfm  34591  2ndmbfm  34592  mbfmcnt  34599  eulerpartlemgh  34709  dstfrvunirn  34806  reprsuc  34943  reprpmtf1o  34954  satfvsucsuc  35752  dmopab3rexdif  35792  cbvabdavw  36653  neifg  36767  filnetlem4  36777  ontgval  36827  bj-gabima  37460  bj-restsn  37607  bj-rest10  37613  bj-restpw  37617  bj-restuni  37622  mptsnunlem  37867  finxpsuclem  37926  wl-clabtv  38124  wl-clabt  38125  poimirlem16  38170  poimirlem19  38173  poimirlem23  38177  poimirlem27  38181  heicant  38189  istotbnd3  38305  sstotbnd  38309  ismtyima  38337  heibor  38355  divrngidl  38562  eccnvep  38822  ecxrn  38940  eqvrelth  39229  disjlem19  39438  prtlem19  39537  prter2  39540  lkrsc  39756  lshpkr  39776  paddvaln0N  40460  paddval0  40469  diaglbN  41714  cdlemm10N  41777  lcfrvalsnN  42200  lcfrlem9  42209  lcdlss  42278  mapd1o  42307  mapd0  42324  hlhillcs  42617  grpods  42846  unitscyglem2  42848  sn-iotalem  42877  fsuppind  43209  mzpmfp  43365  lzunuz  43386  fz1eqin  43387  jm2.23  43610  pw2f1ocnv  43651  dfacbasgrp  43722  nnoeomeqom  43926  oadif1lem  43993  oadif1  43994  fzunt  44068  fzuntd  44069  fzunt1d  44070  fzuntgd  44071  inintabd  44192  cnvcnvintabd  44213  cnvintabd  44216  rfcnpre3  45640  rfcnpre4  45641  iindif2f  45765  rnmptpr  45782  iccshift  46121  iocopn  46123  iooshift  46125  iccintsng  46126  icoopn  46128  limcdm0  46221  limcresiooub  46243  limcresioolb  46244  fperdvper  46520  itgperiod  46582  fourierdlem32  46740  fourierdlem33  46741  fourierdlem48  46755  fourierdlem49  46756  fourierdlem81  46788  fsetsniunop  47670  elsetpreimafvrab  48027  iccpartiun  48067  dfclnbgr6  48505  dfnbgr6  48506  uhgrimisgrgric  48580  clnbgrgrim  48583  stgredgiun  48607  gpgnbgrvtx0  48723  gpgnbgrvtx1  48724  itsclinecirc0in  49435  i0oii  49578  io1ii  49579  sectpropd  49695  invpropd  49697  isopropd  49699  cicpropd  49708  uobffth  49876  uobeqw  49877  natoppfb  49889  oppc1stflem  49945  thincmon  50091  thincepi  50092  termfucterm  50202  grptcmon  50251  grptcepi  50252  lanval2  50285  ranval2  50288  ranval3  50289