Theorem eqrdv 2761

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  eqrdav  2762  abbi  2828  eqabdv  2897  uneq1  4163  unineq  4236  difin2  4249  difsn  4763  intmin4  4942  intprg  4946  iunconst  4966  iinconst  4967  iuneqconst  4968  dfiun2g  4993  iindif1  5040  iindif2  5042  iinin2  5043  iunxsng  5055  iunxsngf  5057  opthprc  5722  dmopab2rex  5911  dmxp  5923  epin  6111  inimasn  6164  dmsnopg  6233  dfco2a  6266  iotaeq  6532  imadif  6654  unima  6991  ssimaex  7001  unpreima  7094  respreima  7097  iinpreima  7101  fnsnbg  7201  fmptsng  7204  fmptsnd  7205  tpres  7238  iunpw  7817  ordpwsuc  7860  ordsucun  7870  fiun  7989  f1iun  7990  reldm  8089  reldmOLD  8090  fimaproj  8189  xpord2pred  8199  xpord3pred  8206  rntpos  8294  onoviun  8389  oarec  8608  iserd  8782  erth  8810  mapdm0  8900  mapfset  8910  ixpiin  8990  boxriin  9006  pw2f1olem  9138  fifo  9461  ordiso2  9546  ttrclse  9765  finacn  10168  acnen  10171  acacni  10258  dfac13  10260  fin23lem26  10442  isf34lem4  10494  axdc3lem2  10568  fpwwe2lem7  10761  fpwwe2lem11  10765  fpwwe2lem12  10766  gch2  10799  gchac  10805  gchina  10823  genpass  11133  1idpr  11153  indpi1  12374  eqreznegel  13101  ixxun  13532  iccid  13561  difreicc  13655  iccsplit  13656  fzsplit2  13723  fzsn  13740  fzpr  13753  uzsplit  13770  fzdif1  13779  preduz  13824  predfz  13827  fz1isolem  14647  pr2pwpr  14665  swrdrn3  14844  isercolllem2  15877  isercoll  15879  bitsmod  16650  bitscmp  16652  saddisj  16679  sadadd  16681  sadass  16685  smupvallem  16697  smueqlem  16704  smumul  16707  gcdcllem2  16714  vdwapun  17196  firest  17653  fncnvimaeqv  18344  mgmhmpropd  18937  mhmpropd  19037  efmnd1bas  19139  subgacs  19421  ecxpid  19436  qsxpid  19437  eqgid  19442  ghmmhmb  19491  ghmpropd  19520  ghmqusnsglem1  19545  ghmquskerlem1  19548  ghmqusker  19552  resscntz  19598  symg1bas  19656  lsmcom2  19920  lsmass  19934  ablnsg  20112  lsmcomx  20121  gsum2d2  20239  subgdmdprd  20301  dprd2d2  20311  2nsgsimpgd  20369  unitpropd  20698  rnghmval2  20725  subsubrng2  20867  subrngpropd  20871  subsubrg2  20902  subrgpropd  20911  rhmpropd  20912  subrgacs  21108  sdrgacs  21109  abvpropd  21143  lssacs  21293  lssats2  21326  lsspropd  21343  lmhmpropd  21399  lbspropd  21425  pzriprnglem10  21851  psdmul  22542  discld  23462  neiptopnei  23505  neiptopreu  23506  restsn  23543  restdis  23551  neitr  23553  restlp  23556  cndis  23664  cnindis  23665  cnpdis  23666  lpcls  23737  hausmapdom  23874  ptpjpre1  23945  tx1cn  23983  tx2cn  23984  hauseqlcld  24020  txkgen  24026  idqtop  24080  tgqtop  24086  acufl  24291  uffix  24295  ufildr  24305  fmfg  24323  rnelfm  24327  fmfnfm  24332  fmid  24334  fmco  24335  flimrest  24357  fclsrest  24398  alexsubALT  24425  tsmsgsum  24513  tsmssubm  24517  tsmsres  24518  tsmsf1o  24519  xpsdsval  24755  blpnf  24771  blin  24795  blres  24805  xmetec  24808  imasf1obl  24862  imasf1oxms  24863  prdsbl  24865  metrest  24898  psmetutop  24941  restmetu  24944  dscopn  24947  cnbl0  25147  bl2ioo  25166  xrtgioo  25181  cncfmet  25285  icoopnst  25315  iocopnst  25316  cldcss2  25818  iunmbl2  25933  mbfmulc2lem  26023  mbfmax  26025  ismbf3d  26030  mbfimaopnlem  26031  mbfaddlem  26036  mbfsup  26040  i1f1lem  26065  i1faddlem  26069  i1fmullem  26070  i1fmulclem  26078  i1fres  26081  mbfi1fseqlem4  26094  limcdif  26251  limcnlp  26253  limcflf  26256  limcres  26261  limcun  26270  ply1remlem  26538  fta1glem2  26542  plypf1  26586  ofmulrt  26655  plyremlem  26680  rnplynfin  26685  aannenlem1  26712  gausslemma2dlem1a  27749  oldlim  28330  negleft  28501  negright  28502  tglineelsb2  29157  tglinecom  29160  angmgmaddcpbl  29447  ushgredgedg  29867  ushgredgedgloop  29869  nbumgrvtx  29984  nbusgrvtxm1uvtx  30043  vdiscusgr  30169  wspniunwspnon  30569  rusgrnumwwlkb0  30620  clwwlknscsh  30710  clwwlknun  30760  eupth2lems  30896  fusgr2wsp2nb  30992  fusgreg2wsp  30994  ubthlem1  31529  ocin  31955  shscom  31978  spansncol  32227  iunsnima  33310  iunsnima2  33311  nfpconfp  33324  unipreima  33335  2ndimaxp  33338  fdifsupp  33375  suppiniseg  33376  ressupprn  33380  1stpreimas  33396  1stpreima  33397  2ndpreima  33398  fpwrelmapffslem  33420  iocinioc2  33467  nndiffz1  33474  fzsplit3  33481  indf1ofs  33529  cntzun  33739  cntzsnid  33740  cntrval2  33831  lindspropd  34042  lsmsnpridl  34055  lsmssass  34057  grplsm0l  34058  grplsmid  34059  nsgqusf1olem2  34069  nsgqusf1olem3  34070  crngmxidl  34098  opprlidlabs  34113  rprmirredb  34168  ressply1mon1p  34203  fldextrspunlsp  34417  irngnzply1  34434  smatrcl  34539  qtophaus  34579  locfinreflem  34583  rspectopn  34610  zarclsiin  34614  rhmpreimacnlem  34627  prsdm  34657  prsrn  34658  1stmbfm  35003  2ndmbfm  35004  mbfmcnt  35011  eulerpartlemgh  35121  dstfrvunirn  35218  reprsuc  35355  reprpmtf1o  35366  satfvsucsuc  36338  dmopab3rexdif  36378  cbvabdavw  37260  neifg  37374  filnetlem4  37384  ontgval  37434  bj-gabima  38068  bj-restsn  38273  bj-rest10  38279  bj-restpw  38283  bj-restuni  38288  mptsnunlem  38529  finxpsuclem  38588  wl-clabtv  38786  wl-clabt  38787  poimirlem16  38822  poimirlem19  38825  poimirlem23  38829  poimirlem27  38833  heicant  38841  istotbnd3  38971  sstotbnd  38975  ismtyima  39003  heibor  39021  divrngidl  39228  eccnvep  39486  ecxrn  39604  eqvrelth  39893  disjlem19  40102  prtlem19  40201  prter2  40204  lkrsc  40420  lshpkr  40440  paddvaln0N  41124  paddval0  41133  diaglbN  42378  cdlemm10N  42441  lcfrvalsnN  42864  lcfrlem9  42873  lcdlss  42942  mapd1o  42971  mapd0  42988  hlhillcs  43281  grpods  43510  unitscyglem2  43512  sn-iotalem  43542  fsuppind  43884  mzpmfp  44024  lzunuz  44045  fz1eqin  44046  jm2.23  44269  pw2f1ocnv  44310  dfacbasgrp  44375  nnoeomeqom  44575  oadif1lem  44642  oadif1  44643  fzunt  44717  fzuntd  44718  fzunt1d  44719  fzuntgd  44720  inintabd  44841  cnvcnvintabd  44861  cnvintabd  44864  rfcnpre3  46324  rfcnpre4  46325  iindif2f  46448  rnmptpr  46465  iccshift  46803  iocopn  46805  iooshift  46807  iccintsng  46808  icoopn  46810  limcdm0  46903  limcresiooub  46925  limcresioolb  46926  fperdvper  47202  itgperiod  47264  fourierdlem32  47422  fourierdlem33  47423  fourierdlem48  47437  fourierdlem49  47438  fourierdlem81  47470  fsetsniunop  48392  elsetpreimafvrab  48749  iccpartiun  48789  dfclnbgr6  49227  dfnbgr6  49228  uhgrimisgrgric  49302  clnbgrgrim  49305  stgredgiun  49329  gpgnbgrvtx0  49445  gpgnbgrvtx1  49446  adcnlaz  49734  itsclinecirc0in  50218  i0oii  50365  io1ii  50366  sectpropd  50482  invpropd  50484  isopropd  50486  cicpropd  50495  uobffth  50665  uobeqw  50666  natoppfb  50684  oppc1stflem  50740  thincmon  50899  thincepi  50900  termfucterm  51013  grptcmon  51062  grptcepi  51063  lanval2  51141  ranval2  51144  ranval3  51145