Theorem eqrdv 2759

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557   = wceq 1559   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  eqrdav  2760  abbi  2826  eqabdv  2894  uneq1  4112  unineq  4238  difin2  4251  difsn  4755  eqsndOLD  4786  intmin4  4932  intprg  4936  iunconst  4956  iinconst  4957  iuneqconst  4958  dfiun2g  4984  iindif1  5029  iindif2  5031  iinin2  5032  iunxsng  5044  iunxsngf  5046  opthprc  5707  dmopab2rex  5889  dmxp  5901  epin  6080  inimasn  6137  dmsnopg  6195  dfco2a  6228  iotaeq  6484  imadif  6600  unima  6937  ssimaex  6947  unpreima  7039  respreima  7042  iinpreima  7045  fnsnbg  7143  fnsnbOLD  7145  fmptsng  7147  fmptsnd  7148  tpres  7180  iunpw  7749  ordpwsuc  7790  ordsucun  7800  fiun  7919  f1iun  7920  reldm  8020  fimaproj  8109  xpord2pred  8119  xpord3pred  8126  rntpos  8213  onoviun  8308  oarec  8525  iserd  8699  erth  8727  mapdm0  8817  mapfset  8825  ixpiin  8900  boxriin  8916  pw2f1olem  9047  fifo  9372  ordiso2  9457  ttrclse  9676  finacn  10000  acnen  10003  acacni  10091  dfac13  10093  fin23lem26  10276  isf34lem4  10328  axdc3lem2  10402  fpwwe2lem7  10589  fpwwe2lem11  10593  fpwwe2lem12  10594  gch2  10627  gchac  10633  gchina  10651  genpass  10961  1idpr  10981  indpi1  12203  eqreznegel  12929  ixxun  13359  iccid  13388  difreicc  13482  iccsplit  13483  fzsplit2  13548  fzsn  13565  fzpr  13578  uzsplit  13595  fzdif1  13604  preduz  13649  predfz  13652  fz1isolem  14468  pr2pwpr  14486  isercolllem2  15684  isercoll  15686  bitsmod  16461  bitscmp  16463  saddisj  16490  sadadd  16492  sadass  16496  smupvallem  16508  smueqlem  16515  smumul  16518  gcdcllem2  16525  vdwapun  17001  firest  17452  fncnvimaeqv  18143  mgmhmpropd  18723  mhmpropd  18817  efmnd1bas  18918  subgacs  19193  eqgid  19212  ghmmhmb  19258  ghmpropd  19287  ghmqusnsglem1  19311  ghmquskerlem1  19314  ghmqusker  19318  resscntz  19364  symg1bas  19422  lsmcom2  19686  lsmass  19700  ablnsg  19878  lsmcomx  19887  gsum2d2  20005  subgdmdprd  20067  dprd2d2  20077  2nsgsimpgd  20135  unitpropd  20453  rnghmval2  20480  subsubrng2  20601  subrngpropd  20605  subsubrg2  20636  subrgpropd  20645  rhmpropd  20646  subrgacs  20837  sdrgacs  20838  abvpropd  20872  lssacs  21022  lssats2  21055  lsspropd  21072  lmhmpropd  21128  lbspropd  21154  pzriprnglem10  21530  psdmul  22219  discld  23137  neiptopnei  23180  neiptopreu  23181  restsn  23218  restdis  23226  neitr  23228  restlp  23231  cndis  23339  cnindis  23340  cnpdis  23341  lpcls  23412  hausmapdom  23548  ptpjpre1  23619  tx1cn  23657  tx2cn  23658  hauseqlcld  23694  txkgen  23700  idqtop  23754  tgqtop  23760  acufl  23965  uffix  23969  ufildr  23979  fmfg  23997  rnelfm  24001  fmfnfm  24006  fmid  24008  fmco  24009  flimrest  24031  fclsrest  24072  alexsubALT  24099  tsmsgsum  24187  tsmssubm  24191  tsmsres  24192  tsmsf1o  24193  xpsdsval  24429  blpnf  24445  blin  24469  blres  24479  xmetec  24482  imasf1obl  24536  imasf1oxms  24537  prdsbl  24539  metrest  24572  psmetutop  24615  restmetu  24618  dscopn  24621  cnbl0  24821  bl2ioo  24840  xrtgioo  24855  cncfmet  24959  icoopnst  24989  iocopnst  24990  cldcss2  25492  iunmbl2  25607  mbfmulc2lem  25697  mbfmax  25699  ismbf3d  25704  mbfimaopnlem  25705  mbfaddlem  25710  mbfsup  25714  i1f1lem  25739  i1faddlem  25743  i1fmullem  25744  i1fmulclem  25752  i1fres  25755  mbfi1fseqlem4  25768  limcdif  25926  limcnlp  25928  limcflf  25931  limcres  25936  limcun  25945  ply1remlem  26213  fta1glem2  26217  plypf1  26260  ofmulrt  26331  plyremlem  26356  aannenlem1  26380  gausslemma2dlem1a  27417  oldlim  27968  negleft  28139  negright  28140  tglineelsb2  28789  tglinecom  28792  ushgredgedg  29387  ushgredgedgloop  29389  nbumgrvtx  29504  nbusgrvtxm1uvtx  29563  vdiscusgr  29689  wspniunwspnon  30080  rusgrnumwwlkb0  30131  clwwlknscsh  30221  clwwlknun  30271  eupth2lems  30397  fusgr2wsp2nb  30493  fusgreg2wsp  30495  ubthlem1  31030  ocin  31456  shscom  31479  spansncol  31728  iunsnima  32781  iunsnima2  32782  nfpconfp  32795  unipreima  32806  2ndimaxp  32809  fdifsupp  32848  suppiniseg  32849  ressupprn  32853  1stpreimas  32869  1stpreima  32870  2ndpreima  32871  fpwrelmapffslem  32895  iocinioc2  32942  nndiffz1  32949  fzsplit3  32956  indf1ofs  33005  swrdrn3  33094  cntzun  33220  cntzsnid  33221  cntrval2  33312  ecxpid  33508  qsxpid  33509  lindspropd  33530  lsmsnpridl  33545  lsmssass  33549  grplsm0l  33550  grplsmid  33551  nsgqusf1olem2  33561  nsgqusf1olem3  33562  crngmxidl  33618  opprlidlabs  33634  rprmirredb  33689  ressply1mon1p  33725  fldextrspunlsp  33932  irngnzply1  33949  smatrcl  34054  qtophaus  34094  locfinreflem  34098  rspectopn  34125  zarclsiin  34129  rhmpreimacnlem  34142  prsdm  34172  prsrn  34173  1stmbfm  34518  2ndmbfm  34519  mbfmcnt  34526  eulerpartlemgh  34636  dstfrvunirn  34733  reprsuc  34870  reprpmtf1o  34881  satfvsucsuc  35676  dmopab3rexdif  35716  cbvabdavw  36577  neifg  36692  filnetlem4  36702  ontgval  36752  bj-gabima  37386  bj-restsn  37533  bj-rest10  37539  bj-restpw  37543  bj-restuni  37548  mptsnunlem  37793  finxpsuclem  37852  wl-clabtv  38050  wl-clabt  38051  poimirlem16  38096  poimirlem19  38099  poimirlem23  38103  poimirlem27  38107  heicant  38115  istotbnd3  38231  sstotbnd  38235  ismtyima  38263  heibor  38281  divrngidl  38488  eccnvep  38748  ecxrn  38866  eqvrelth  39155  disjlem19  39364  prtlem19  39463  prter2  39466  lkrsc  39682  lshpkr  39702  paddvaln0N  40386  paddval0  40395  diaglbN  41640  cdlemm10N  41703  lcfrvalsnN  42126  lcfrlem9  42135  lcdlss  42204  mapd1o  42233  mapd0  42250  hlhillcs  42543  grpods  42772  unitscyglem2  42774  sn-iotalem  42801  fsuppind  43133  mzpmfp  43289  lzunuz  43310  fz1eqin  43311  jm2.23  43534  pw2f1ocnv  43575  dfacbasgrp  43646  nnoeomeqom  43850  oadif1lem  43917  oadif1  43918  fzunt  43992  fzuntd  43993  fzunt1d  43994  fzuntgd  43995  inintabd  44116  cnvcnvintabd  44137  cnvintabd  44140  rfcnpre3  45574  rfcnpre4  45575  iindif2f  45699  rnmptpr  45716  iccshift  46055  iocopn  46057  iooshift  46059  iccintsng  46060  icoopn  46062  limcdm0  46155  limcresiooub  46177  limcresioolb  46178  fperdvper  46454  itgperiod  46516  fourierdlem32  46674  fourierdlem33  46675  fourierdlem48  46689  fourierdlem49  46690  fourierdlem81  46722  fsetsniunop  47604  elsetpreimafvrab  47961  iccpartiun  48001  dfclnbgr6  48439  dfnbgr6  48440  uhgrimisgrgric  48514  clnbgrgrim  48517  stgredgiun  48541  gpgnbgrvtx0  48657  gpgnbgrvtx1  48658  itsclinecirc0in  49358  i0oii  49502  io1ii  49503  sectpropd  49619  invpropd  49621  isopropd  49623  cicpropd  49632  uobffth  49800  uobeqw  49801  natoppfb  49813  oppc1stflem  49869  thincmon  50015  thincepi  50016  termfucterm  50126  grptcmon  50175  grptcepi  50176  lanval2  50209  ranval2  50212  ranval3  50213