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  4124  unineq  4251  difin2  4264  difsn  4762  eqsndOLD  4795  intmin4  4941  iunconst  4965  iinconst  4966  iuneqconst  4967  dfiun2g  4994  dfiun2gOLD  4995  iindif1  5039  iindif2  5041  iinin2  5042  iunxsng  5054  iunxsngf  5056  opthprc  5702  dmopab2rex  5881  dmxp  5892  epin  6066  inimasn  6129  dmsnopg  6186  dfco2a  6219  iotaeq  6476  imadif  6600  unima  6936  ssimaex  6946  unpreima  7035  respreima  7038  iinpreima  7041  fnsnbg  7138  fnsnbOLD  7140  fmptsng  7142  fmptsnd  7143  tpres  7175  iunpw  7747  ordpwsuc  7790  ordsucun  7800  fiun  7921  f1iun  7922  reldm  8023  fimaproj  8114  xpord2pred  8124  xpord3pred  8131  rntpos  8218  onoviun  8312  oarec  8526  iserd  8697  erth  8725  mapdm0  8815  mapfset  8823  ixpiin  8897  boxriin  8913  pw2f1olem  9045  fifo  9383  ordiso2  9468  ttrclse  9680  finacn  10003  acnen  10006  acacni  10094  dfac13  10096  fin23lem26  10278  isf34lem4  10330  axdc3lem2  10404  fpwwe2lem7  10590  fpwwe2lem11  10594  fpwwe2lem12  10595  gch2  10628  gchac  10634  gchina  10652  genpass  10962  1idpr  10982  eqreznegel  12893  ixxun  13322  iccid  13351  difreicc  13445  iccsplit  13446  fzsplit2  13510  fzsn  13527  fzpr  13540  uzsplit  13557  fzdif1  13566  preduz  13611  predfz  13614  fz1isolem  14426  pr2pwpr  14444  isercolllem2  15632  isercoll  15634  bitsmod  16406  bitscmp  16408  saddisj  16435  sadadd  16437  sadass  16441  smupvallem  16453  smueqlem  16460  smumul  16463  gcdcllem2  16470  vdwapun  16945  firest  17395  fncnvimaeqv  18081  mgmhmpropd  18625  mhmpropd  18719  efmnd1bas  18820  subgacs  19093  eqgid  19112  ghmmhmb  19159  ghmpropd  19188  ghmqusnsglem1  19212  ghmquskerlem1  19215  ghmqusker  19219  resscntz  19265  symg1bas  19321  lsmcom2  19585  lsmass  19599  ablnsg  19777  lsmcomx  19786  gsum2d2  19904  subgdmdprd  19966  dprd2d2  19976  2nsgsimpgd  20034  unitpropd  20326  rnghmval2  20353  subsubrng2  20473  subrngpropd  20477  subsubrg2  20508  subrgpropd  20517  rhmpropd  20518  subrgacs  20709  sdrgacs  20710  abvpropd  20744  lssacs  20873  lssats2  20906  lsspropd  20924  lmhmpropd  20980  lbspropd  21006  pzriprnglem10  21400  psdmul  22053  discld  22976  neiptopnei  23019  neiptopreu  23020  restsn  23057  restdis  23065  neitr  23067  restlp  23070  cndis  23178  cnindis  23179  cnpdis  23180  lpcls  23251  hausmapdom  23387  ptpjpre1  23458  tx1cn  23496  tx2cn  23497  hauseqlcld  23533  txkgen  23539  idqtop  23593  tgqtop  23599  acufl  23804  uffix  23808  ufildr  23818  fmfg  23836  rnelfm  23840  fmfnfm  23845  fmid  23847  fmco  23848  flimrest  23870  fclsrest  23911  alexsubALT  23938  tsmsgsum  24026  tsmssubm  24030  tsmsres  24031  tsmsf1o  24032  xpsdsval  24269  blpnf  24285  blin  24309  blres  24319  xmetec  24322  imasf1obl  24376  imasf1oxms  24377  prdsbl  24379  metrest  24412  psmetutop  24455  restmetu  24458  dscopn  24461  cnbl0  24661  bl2ioo  24680  xrtgioo  24695  cncfmet  24802  icoopnst  24836  iocopnst  24837  cldcss2  25342  iunmbl2  25458  mbfmulc2lem  25548  mbfmax  25550  ismbf3d  25555  mbfimaopnlem  25556  mbfaddlem  25561  mbfsup  25565  i1f1lem  25590  i1faddlem  25594  i1fmullem  25595  i1fmulclem  25603  i1fres  25606  mbfi1fseqlem4  25619  limcdif  25777  limcnlp  25779  limcflf  25782  limcres  25787  limcun  25796  ply1remlem  26070  fta1glem2  26074  plypf1  26117  ofmulrt  26189  plyremlem  26212  aannenlem1  26236  gausslemma2dlem1a  27276  oldlim  27798  tglineelsb2  28559  tglinecom  28562  ushgredgedg  29156  ushgredgedgloop  29158  nbumgrvtx  29273  nbusgrvtxm1uvtx  29332  vdiscusgr  29459  wspniunwspnon  29853  rusgrnumwwlkb0  29901  clwwlknscsh  29991  clwwlknun  30041  eupth2lems  30167  fusgr2wsp2nb  30263  fusgreg2wsp  30265  ubthlem1  30799  ocin  31225  shscom  31248  spansncol  31497  iunsnima  32546  iunsnima2  32547  nfpconfp  32556  unipreima  32567  2ndimaxp  32570  fdifsupp  32608  suppiniseg  32609  ressupprn  32613  1stpreimas  32629  1stpreima  32630  2ndpreima  32631  fpwrelmapffslem  32655  iocinioc2  32702  nndiffz1  32709  fzsplit3  32716  indpi1  32783  indf1ofs  32789  swrdrn3  32877  cntzun  33008  cntzsnid  33009  cntrval2  33128  ecxpid  33332  qsxpid  33333  lindspropd  33354  lsmsnpridl  33369  lsmssass  33373  grplsm0l  33374  grplsmid  33375  nsgqusf1olem2  33385  nsgqusf1olem3  33386  crngmxidl  33440  opprlidlabs  33456  rprmirredb  33503  ressply1mon1p  33537  fldextrspunlsp  33669  irngnzply1  33686  smatrcl  33786  qtophaus  33826  locfinreflem  33830  rspectopn  33857  zarclsiin  33861  rhmpreimacnlem  33874  prsdm  33904  prsrn  33905  1stmbfm  34251  2ndmbfm  34252  mbfmcnt  34259  eulerpartlemgh  34369  dstfrvunirn  34466  reprsuc  34606  reprpmtf1o  34617  satfvsucsuc  35352  dmopab3rexdif  35392  cbvabdavw  36244  neifg  36359  filnetlem4  36369  ontgval  36419  bj-gabima  36928  bj-restsn  37070  bj-rest10  37076  bj-restpw  37080  bj-restuni  37085  mptsnunlem  37326  finxpsuclem  37385  wl-clabtv  37585  wl-clabt  37586  poimirlem16  37630  poimirlem19  37633  poimirlem23  37637  poimirlem27  37641  heicant  37649  istotbnd3  37765  sstotbnd  37769  ismtyima  37797  heibor  37815  divrngidl  38022  eccnvep  38270  ecxrn  38373  eqvrelth  38602  disjlem19  38793  prtlem19  38871  prter2  38874  lkrsc  39090  lshpkr  39110  paddvaln0N  39795  paddval0  39804  diaglbN  41049  cdlemm10N  41112  lcfrvalsnN  41535  lcfrlem9  41544  lcdlss  41613  mapd1o  41642  mapd0  41659  hlhillcs  41952  grpods  42182  unitscyglem2  42184  sn-iotalem  42209  fsuppind  42578  mzpmfp  42735  lzunuz  42756  fz1eqin  42757  jm2.23  42985  pw2f1ocnv  43026  dfacbasgrp  43097  nnoeomeqom  43301  oadif1lem  43368  oadif1  43369  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  inintabd  43568  cnvcnvintabd  43589  cnvintabd  43592  rfcnpre3  45027  rfcnpre4  45028  iindif2f  45154  rnmptpr  45171  iccshift  45516  iocopn  45518  iooshift  45520  iccintsng  45521  icoopn  45523  limcdm0  45616  limcresiooub  45640  limcresioolb  45641  fperdvper  45917  itgperiod  45979  fourierdlem32  46137  fourierdlem33  46138  fourierdlem48  46152  fourierdlem49  46153  fourierdlem81  46185  fsetsniunop  47050  elsetpreimafvrab  47395  iccpartiun  47435  dfclnbgr6  47856  dfnbgr6  47857  uhgrimisgrgric  47931  clnbgrgrim  47934  stgredgiun  47957  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  itsclinecirc0in  48764  i0oii  48908  io1ii  48909  sectpropd  49026  invpropd  49028  isopropd  49030  cicpropd  49039  uobffth  49207  uobeqw  49208  natoppfb  49220  oppc1stflem  49276  thincmon  49422  thincepi  49423  termfucterm  49533  grptcmon  49582  grptcepi  49583  lanval2  49616  ranval2  49619  ranval3  49620