Theorem eqrdv 2727

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eqrdav  2728  abbi  2794  eqabdv  2861  uneq1  4114  unineq  4241  difin2  4254  difsn  4752  eqsndOLD  4785  intmin4  4930  iunconst  4954  iinconst  4955  iuneqconst  4956  dfiun2g  4983  iindif1  5027  iindif2  5029  iinin2  5030  iunxsng  5042  iunxsngf  5044  opthprc  5687  dmopab2rex  5864  dmxp  5875  epin  6050  inimasn  6109  dmsnopg  6166  dfco2a  6199  iotaeq  6454  imadif  6570  unima  6902  ssimaex  6912  unpreima  7001  respreima  7004  iinpreima  7007  fnsnbg  7104  fnsnbOLD  7106  fmptsng  7108  fmptsnd  7109  tpres  7141  iunpw  7711  ordpwsuc  7754  ordsucun  7764  fiun  7885  f1iun  7886  reldm  7986  fimaproj  8075  xpord2pred  8085  xpord3pred  8092  rntpos  8179  onoviun  8273  oarec  8487  iserd  8658  erth  8686  mapdm0  8776  mapfset  8784  ixpiin  8858  boxriin  8874  pw2f1olem  9005  fifo  9341  ordiso2  9426  ttrclse  9642  finacn  9963  acnen  9966  acacni  10054  dfac13  10056  fin23lem26  10238  isf34lem4  10290  axdc3lem2  10364  fpwwe2lem7  10550  fpwwe2lem11  10554  fpwwe2lem12  10555  gch2  10588  gchac  10594  gchina  10612  genpass  10922  1idpr  10942  eqreznegel  12854  ixxun  13283  iccid  13312  difreicc  13406  iccsplit  13407  fzsplit2  13471  fzsn  13488  fzpr  13501  uzsplit  13518  fzdif1  13527  preduz  13572  predfz  13575  fz1isolem  14387  pr2pwpr  14405  isercolllem2  15592  isercoll  15594  bitsmod  16366  bitscmp  16368  saddisj  16395  sadadd  16397  sadass  16401  smupvallem  16413  smueqlem  16420  smumul  16423  gcdcllem2  16430  vdwapun  16905  firest  17355  fncnvimaeqv  18045  mgmhmpropd  18591  mhmpropd  18685  efmnd1bas  18786  subgacs  19059  eqgid  19078  ghmmhmb  19125  ghmpropd  19154  ghmqusnsglem1  19178  ghmquskerlem1  19181  ghmqusker  19185  resscntz  19231  symg1bas  19289  lsmcom2  19553  lsmass  19567  ablnsg  19745  lsmcomx  19754  gsum2d2  19872  subgdmdprd  19934  dprd2d2  19944  2nsgsimpgd  20002  unitpropd  20321  rnghmval2  20348  subsubrng2  20468  subrngpropd  20472  subsubrg2  20503  subrgpropd  20512  rhmpropd  20513  subrgacs  20704  sdrgacs  20705  abvpropd  20739  lssacs  20889  lssats2  20922  lsspropd  20940  lmhmpropd  20996  lbspropd  21022  pzriprnglem10  21416  psdmul  22070  discld  22993  neiptopnei  23036  neiptopreu  23037  restsn  23074  restdis  23082  neitr  23084  restlp  23087  cndis  23195  cnindis  23196  cnpdis  23197  lpcls  23268  hausmapdom  23404  ptpjpre1  23475  tx1cn  23513  tx2cn  23514  hauseqlcld  23550  txkgen  23556  idqtop  23610  tgqtop  23616  acufl  23821  uffix  23825  ufildr  23835  fmfg  23853  rnelfm  23857  fmfnfm  23862  fmid  23864  fmco  23865  flimrest  23887  fclsrest  23928  alexsubALT  23955  tsmsgsum  24043  tsmssubm  24047  tsmsres  24048  tsmsf1o  24049  xpsdsval  24286  blpnf  24302  blin  24326  blres  24336  xmetec  24339  imasf1obl  24393  imasf1oxms  24394  prdsbl  24396  metrest  24429  psmetutop  24472  restmetu  24475  dscopn  24478  cnbl0  24678  bl2ioo  24697  xrtgioo  24712  cncfmet  24819  icoopnst  24853  iocopnst  24854  cldcss2  25359  iunmbl2  25475  mbfmulc2lem  25565  mbfmax  25567  ismbf3d  25572  mbfimaopnlem  25573  mbfaddlem  25578  mbfsup  25582  i1f1lem  25607  i1faddlem  25611  i1fmullem  25612  i1fmulclem  25620  i1fres  25623  mbfi1fseqlem4  25636  limcdif  25794  limcnlp  25796  limcflf  25799  limcres  25804  limcun  25813  ply1remlem  26087  fta1glem2  26091  plypf1  26134  ofmulrt  26206  plyremlem  26229  aannenlem1  26253  gausslemma2dlem1a  27293  oldlim  27820  tglineelsb2  28596  tglinecom  28599  ushgredgedg  29193  ushgredgedgloop  29195  nbumgrvtx  29310  nbusgrvtxm1uvtx  29369  vdiscusgr  29496  wspniunwspnon  29887  rusgrnumwwlkb0  29935  clwwlknscsh  30025  clwwlknun  30075  eupth2lems  30201  fusgr2wsp2nb  30297  fusgreg2wsp  30299  ubthlem1  30833  ocin  31259  shscom  31282  spansncol  31531  iunsnima  32582  iunsnima2  32583  nfpconfp  32594  unipreima  32605  2ndimaxp  32608  fdifsupp  32646  suppiniseg  32647  ressupprn  32651  1stpreimas  32667  1stpreima  32668  2ndpreima  32669  fpwrelmapffslem  32694  iocinioc2  32741  nndiffz1  32748  fzsplit3  32755  indpi1  32822  indf1ofs  32828  swrdrn3  32916  cntzun  33040  cntzsnid  33041  cntrval2  33132  ecxpid  33317  qsxpid  33318  lindspropd  33339  lsmsnpridl  33354  lsmssass  33358  grplsm0l  33359  grplsmid  33360  nsgqusf1olem2  33370  nsgqusf1olem3  33371  crngmxidl  33425  opprlidlabs  33441  rprmirredb  33488  ressply1mon1p  33522  fldextrspunlsp  33660  irngnzply1  33677  smatrcl  33782  qtophaus  33822  locfinreflem  33826  rspectopn  33853  zarclsiin  33857  rhmpreimacnlem  33870  prsdm  33900  prsrn  33901  1stmbfm  34247  2ndmbfm  34248  mbfmcnt  34255  eulerpartlemgh  34365  dstfrvunirn  34462  reprsuc  34602  reprpmtf1o  34613  satfvsucsuc  35357  dmopab3rexdif  35397  cbvabdavw  36249  neifg  36364  filnetlem4  36374  ontgval  36424  bj-gabima  36933  bj-restsn  37075  bj-rest10  37081  bj-restpw  37085  bj-restuni  37090  mptsnunlem  37331  finxpsuclem  37390  wl-clabtv  37590  wl-clabt  37591  poimirlem16  37635  poimirlem19  37638  poimirlem23  37642  poimirlem27  37646  heicant  37654  istotbnd3  37770  sstotbnd  37774  ismtyima  37802  heibor  37820  divrngidl  38027  eccnvep  38275  ecxrn  38378  eqvrelth  38607  disjlem19  38798  prtlem19  38876  prter2  38879  lkrsc  39095  lshpkr  39115  paddvaln0N  39800  paddval0  39809  diaglbN  41054  cdlemm10N  41117  lcfrvalsnN  41540  lcfrlem9  41549  lcdlss  41618  mapd1o  41647  mapd0  41664  hlhillcs  41957  grpods  42187  unitscyglem2  42189  sn-iotalem  42214  fsuppind  42583  mzpmfp  42740  lzunuz  42761  fz1eqin  42762  jm2.23  42989  pw2f1ocnv  43030  dfacbasgrp  43101  nnoeomeqom  43305  oadif1lem  43372  oadif1  43373  fzunt  43448  fzuntd  43449  fzunt1d  43450  fzuntgd  43451  inintabd  43572  cnvcnvintabd  43593  cnvintabd  43596  rfcnpre3  45031  rfcnpre4  45032  iindif2f  45158  rnmptpr  45175  iccshift  45519  iocopn  45521  iooshift  45523  iccintsng  45524  icoopn  45526  limcdm0  45619  limcresiooub  45643  limcresioolb  45644  fperdvper  45920  itgperiod  45982  fourierdlem32  46140  fourierdlem33  46141  fourierdlem48  46155  fourierdlem49  46156  fourierdlem81  46188  fsetsniunop  47053  elsetpreimafvrab  47398  iccpartiun  47438  dfclnbgr6  47860  dfnbgr6  47861  uhgrimisgrgric  47935  clnbgrgrim  47938  stgredgiun  47962  gpgnbgrvtx0  48078  gpgnbgrvtx1  48079  itsclinecirc0in  48780  i0oii  48924  io1ii  48925  sectpropd  49042  invpropd  49044  isopropd  49046  cicpropd  49055  uobffth  49223  uobeqw  49224  natoppfb  49236  oppc1stflem  49292  thincmon  49438  thincepi  49439  termfucterm  49549  grptcmon  49598  grptcepi  49599  lanval2  49632  ranval2  49635  ranval3  49636