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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   = wceq 1541   ∈ wcel 2106

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqrdav  2736  abbi1  2805  abbi2dv  2876  ss2abdv  4011  uneq1  4107  unineq  4228  difin2  4242  difsn  4749  intmin4  4929  iunconst  4954  iinconst  4955  iuneqconst  4956  dfiun2g  4981  dfiun2gOLD  4982  iindif1  5026  iindif2  5028  iinin2  5029  iunxsng  5041  iunxsngf  5043  opthprc  5686  dmopab2rex  5863  epin  6037  inimasn  6098  dmsnopg  6155  dfco2a  6188  iotaeq  6448  imadif  6572  unima  6903  ssimaex  6913  unpreima  7000  respreima  7003  iinpreima  7006  fnsnb  7098  fmptsng  7100  fmptsnd  7101  tpres  7136  iunpw  7687  ordpwsuc  7732  ordsucun  7742  fiun  7857  f1iun  7858  reldm  7957  fimaproj  8047  rntpos  8129  onoviun  8248  oarec  8468  iserd  8599  erth  8622  mapdm0  8705  mapfset  8713  ixpiin  8787  boxriin  8803  pw2f1olem  8945  fifo  9293  ordiso2  9376  ttrclse  9588  finacn  9911  acnen  9914  acacni  10001  dfac13  10003  fin23lem26  10186  isf34lem4  10238  axdc3lem2  10312  fpwwe2lem7  10498  fpwwe2lem11  10502  fpwwe2lem12  10503  gch2  10536  gchac  10542  gchina  10560  genpass  10870  1idpr  10890  eqreznegel  12779  ixxun  13200  iccid  13229  difreicc  13321  iccsplit  13322  fzsplit2  13386  fzsn  13403  fzpr  13416  uzsplit  13433  preduz  13483  predfz  13486  fz1isolem  14279  pr2pwpr  14297  isercolllem2  15476  isercoll  15478  bitsmod  16242  bitscmp  16244  saddisj  16271  sadadd  16273  sadass  16277  smupvallem  16289  smueqlem  16296  smumul  16299  gcdcllem2  16306  vdwapun  16772  firest  17240  fncnvimaeqv  17933  mhmpropd  18533  efmnd1bas  18628  subgacs  18885  eqgid  18904  ghmmhmb  18941  ghmpropd  18968  resscntz  19034  symg1bas  19094  lsmcom2  19356  lsmass  19370  ablnsg  19543  lsmcomx  19552  gsum2d2  19669  subgdmdprd  19731  dprd2d2  19741  2nsgsimpgd  19799  unitpropd  20033  subsubrg2  20155  subrgpropd  20163  rhmpropd  20164  subrgacs  20173  sdrgacs  20174  abvpropd  20207  lssacs  20334  lssats2  20367  lsspropd  20384  lmhmpropd  20440  lbspropd  20466  discld  22345  neiptopnei  22388  neiptopreu  22389  restsn  22426  restdis  22434  neitr  22436  restlp  22439  cndis  22547  cnindis  22548  cnpdis  22549  lpcls  22620  hausmapdom  22756  ptpjpre1  22827  tx1cn  22865  tx2cn  22866  hauseqlcld  22902  txkgen  22908  idqtop  22962  tgqtop  22968  acufl  23173  uffix  23177  ufildr  23187  fmfg  23205  rnelfm  23209  fmfnfm  23214  fmid  23216  fmco  23217  flimrest  23239  fclsrest  23280  alexsubALT  23307  tsmsgsum  23395  tsmssubm  23399  tsmsres  23400  tsmsf1o  23401  xpsdsval  23639  blpnf  23655  blin  23679  blres  23689  xmetec  23692  imasf1obl  23749  imasf1oxms  23750  prdsbl  23752  metrest  23785  psmetutop  23828  restmetu  23831  dscopn  23834  cnbl0  24042  bl2ioo  24060  xrtgioo  24074  cncfmet  24177  icoopnst  24207  iocopnst  24208  cldcss2  24711  iunmbl2  24826  mbfmulc2lem  24916  mbfmax  24918  ismbf3d  24923  mbfimaopnlem  24924  mbfaddlem  24929  mbfsup  24933  i1f1lem  24958  i1faddlem  24962  i1fmullem  24963  i1fmulclem  24972  i1fres  24975  mbfi1fseqlem4  24988  limcdif  25145  limcnlp  25147  limcflf  25150  limcres  25155  limcun  25164  ply1remlem  25432  fta1glem2  25436  plypf1  25478  ofmulrt  25547  plyremlem  25569  aannenlem1  25593  gausslemma2dlem1a  26618  tglineelsb2  27281  tglinecom  27284  ushgredgedg  27884  ushgredgedgloop  27886  nbumgrvtx  28001  nbusgrvtxm1uvtx  28060  vdiscusgr  28186  wspniunwspnon  28575  rusgrnumwwlkb0  28623  clwwlknscsh  28713  clwwlknun  28763  eupth2lems  28889  fusgr2wsp2nb  28985  fusgreg2wsp  28987  ubthlem1  29519  ocin  29945  shscom  29968  spansncol  30217  eqsnd  31162  iunsnima  31243  iunsnima2  31244  nfpconfp  31252  unipreima  31266  2ndimaxp  31269  suppiniseg  31305  ressupprn  31309  1stpreimas  31323  1stpreima  31324  2ndpreima  31325  fpwrelmapffslem  31352  iocinioc2  31385  nndiffz1  31392  fzsplit3  31400  swrdrn3  31512  cntzun  31605  cntzsnid  31606  ecxpid  31850  qsxpid  31852  lindspropd  31872  lsmsnpridl  31881  lsmssass  31885  grplsm0l  31886  grplsmid  31887  nsgqusf1olem2  31894  nsgqusf1olem3  31895  smatrcl  32042  qtophaus  32082  locfinreflem  32086  rspectopn  32113  zarclsiin  32117  rhmpreimacnlem  32130  prsdm  32160  prsrn  32161  indpi1  32284  indf1ofs  32290  1stmbfm  32525  2ndmbfm  32526  mbfmcnt  32533  eulerpartlemgh  32643  dstfrvunirn  32739  reprsuc  32893  reprpmtf1o  32904  satfvsucsuc  33624  dmopab3rexdif  33664  xpord2pred  34074  xpord3pred  34080  oldlim  34177  neifg  34697  filnetlem4  34707  ontgval  34757  bj-gabima  35264  bj-restsn  35407  bj-rest10  35413  bj-restpw  35417  bj-restuni  35422  mptsnunlem  35663  finxpsuclem  35722  wl-clabtv  35904  wl-clabt  35905  poimirlem16  35949  poimirlem19  35952  poimirlem23  35956  poimirlem27  35960  heicant  35968  istotbnd3  36085  sstotbnd  36089  ismtyima  36117  heibor  36135  divrngidl  36342  eccnvep  36598  ecxrn  36705  eqvrelth  36929  disjlem19  37119  prtlem19  37196  prter2  37199  lkrsc  37415  lshpkr  37435  paddvaln0N  38120  paddval0  38129  diaglbN  39374  cdlemm10N  39437  lcfrvalsnN  39860  lcfrlem9  39869  lcdlss  39938  mapd1o  39967  mapd0  39984  hlhillcs  40281  sn-iotalem  40498  fnsnbt  40511  fsuppind  40590  mzpmfp  40882  lzunuz  40903  fz1eqin  40904  jm2.23  41132  pw2f1ocnv  41173  dfacbasgrp  41247  fzunt  41436  fzuntd  41437  fzunt1d  41438  fzuntgd  41439  inintabd  41560  cnvcnvintabd  41581  cnvintabd  41584  rfcnpre3  42949  rfcnpre4  42950  rnmptpr  43092  iccshift  43444  iocopn  43446  iooshift  43448  iccintsng  43449  icoopn  43451  limcdm0  43547  limcresiooub  43571  limcresioolb  43572  fperdvper  43848  itgperiod  43910  fourierdlem32  44068  fourierdlem33  44069  fourierdlem48  44083  fourierdlem49  44084  fourierdlem81  44116  fsetsniunop  44961  elsetpreimafvrab  45264  iccpartiun  45304  mgmhmpropd  45757  rnghmval2  45871  itsclinecirc0in  46539  i0oii  46631  io1ii  46632  thincmon  46733  thincepi  46734  grptcmon  46795  grptcepi  46796