Theorem eqrdv 2729

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  eqrdav  2730  abbi  2796  eqabdv  2864  uneq1  4106  unineq  4233  difin2  4246  difsn  4745  eqsndOLD  4778  intmin4  4922  iunconst  4946  iinconst  4947  iuneqconst  4948  dfiun2g  4975  iindif1  5018  iindif2  5020  iinin2  5021  iunxsng  5033  iunxsngf  5035  opthprc  5675  dmopab2rex  5852  dmxp  5864  epin  6039  inimasn  6098  dmsnopg  6155  dfco2a  6188  iotaeq  6444  imadif  6560  unima  6892  ssimaex  6902  unpreima  6991  respreima  6994  iinpreima  6997  fnsnbg  7093  fnsnbOLD  7095  fmptsng  7097  fmptsnd  7098  tpres  7130  iunpw  7699  ordpwsuc  7740  ordsucun  7750  fiun  7870  f1iun  7871  reldm  7971  fimaproj  8060  xpord2pred  8070  xpord3pred  8077  rntpos  8164  onoviun  8258  oarec  8472  iserd  8643  erth  8671  mapdm0  8761  mapfset  8769  ixpiin  8843  boxriin  8859  pw2f1olem  8989  fifo  9311  ordiso2  9396  ttrclse  9612  finacn  9936  acnen  9939  acacni  10027  dfac13  10029  fin23lem26  10211  isf34lem4  10263  axdc3lem2  10337  fpwwe2lem7  10523  fpwwe2lem11  10527  fpwwe2lem12  10528  gch2  10561  gchac  10567  gchina  10585  genpass  10895  1idpr  10915  eqreznegel  12827  ixxun  13256  iccid  13285  difreicc  13379  iccsplit  13380  fzsplit2  13444  fzsn  13461  fzpr  13474  uzsplit  13491  fzdif1  13500  preduz  13545  predfz  13548  fz1isolem  14363  pr2pwpr  14381  isercolllem2  15568  isercoll  15570  bitsmod  16342  bitscmp  16344  saddisj  16371  sadadd  16373  sadass  16377  smupvallem  16389  smueqlem  16396  smumul  16399  gcdcllem2  16406  vdwapun  16881  firest  17331  fncnvimaeqv  18021  mgmhmpropd  18601  mhmpropd  18695  efmnd1bas  18796  subgacs  19068  eqgid  19087  ghmmhmb  19134  ghmpropd  19163  ghmqusnsglem1  19187  ghmquskerlem1  19190  ghmqusker  19194  resscntz  19240  symg1bas  19298  lsmcom2  19562  lsmass  19576  ablnsg  19754  lsmcomx  19763  gsum2d2  19881  subgdmdprd  19943  dprd2d2  19953  2nsgsimpgd  20011  unitpropd  20330  rnghmval2  20357  subsubrng2  20474  subrngpropd  20478  subsubrg2  20509  subrgpropd  20518  rhmpropd  20519  subrgacs  20710  sdrgacs  20711  abvpropd  20745  lssacs  20895  lssats2  20928  lsspropd  20946  lmhmpropd  21002  lbspropd  21028  pzriprnglem10  21422  psdmul  22076  discld  22999  neiptopnei  23042  neiptopreu  23043  restsn  23080  restdis  23088  neitr  23090  restlp  23093  cndis  23201  cnindis  23202  cnpdis  23203  lpcls  23274  hausmapdom  23410  ptpjpre1  23481  tx1cn  23519  tx2cn  23520  hauseqlcld  23556  txkgen  23562  idqtop  23616  tgqtop  23622  acufl  23827  uffix  23831  ufildr  23841  fmfg  23859  rnelfm  23863  fmfnfm  23868  fmid  23870  fmco  23871  flimrest  23893  fclsrest  23934  alexsubALT  23961  tsmsgsum  24049  tsmssubm  24053  tsmsres  24054  tsmsf1o  24055  xpsdsval  24291  blpnf  24307  blin  24331  blres  24341  xmetec  24344  imasf1obl  24398  imasf1oxms  24399  prdsbl  24401  metrest  24434  psmetutop  24477  restmetu  24480  dscopn  24483  cnbl0  24683  bl2ioo  24702  xrtgioo  24717  cncfmet  24824  icoopnst  24858  iocopnst  24859  cldcss2  25364  iunmbl2  25480  mbfmulc2lem  25570  mbfmax  25572  ismbf3d  25577  mbfimaopnlem  25578  mbfaddlem  25583  mbfsup  25587  i1f1lem  25612  i1faddlem  25616  i1fmullem  25617  i1fmulclem  25625  i1fres  25628  mbfi1fseqlem4  25641  limcdif  25799  limcnlp  25801  limcflf  25804  limcres  25809  limcun  25818  ply1remlem  26092  fta1glem2  26096  plypf1  26139  ofmulrt  26211  plyremlem  26234  aannenlem1  26258  gausslemma2dlem1a  27298  oldlim  27827  tglineelsb2  28605  tglinecom  28608  ushgredgedg  29202  ushgredgedgloop  29204  nbumgrvtx  29319  nbusgrvtxm1uvtx  29378  vdiscusgr  29505  wspniunwspnon  29896  rusgrnumwwlkb0  29944  clwwlknscsh  30034  clwwlknun  30084  eupth2lems  30210  fusgr2wsp2nb  30306  fusgreg2wsp  30308  ubthlem1  30842  ocin  31268  shscom  31291  spansncol  31540  iunsnima  32593  iunsnima2  32594  nfpconfp  32606  unipreima  32617  2ndimaxp  32620  fdifsupp  32658  suppiniseg  32659  ressupprn  32663  1stpreimas  32679  1stpreima  32680  2ndpreima  32681  fpwrelmapffslem  32707  iocinioc2  32754  nndiffz1  32761  fzsplit3  32768  indpi1  32833  indf1ofs  32839  swrdrn3  32928  cntzun  33040  cntzsnid  33041  cntrval2  33132  ecxpid  33318  qsxpid  33319  lindspropd  33340  lsmsnpridl  33355  lsmssass  33359  grplsm0l  33360  grplsmid  33361  nsgqusf1olem2  33371  nsgqusf1olem3  33372  crngmxidl  33426  opprlidlabs  33442  rprmirredb  33489  ressply1mon1p  33523  fldextrspunlsp  33679  irngnzply1  33696  smatrcl  33801  qtophaus  33841  locfinreflem  33845  rspectopn  33872  zarclsiin  33876  rhmpreimacnlem  33889  prsdm  33919  prsrn  33920  1stmbfm  34265  2ndmbfm  34266  mbfmcnt  34273  eulerpartlemgh  34383  dstfrvunirn  34480  reprsuc  34620  reprpmtf1o  34631  satfvsucsuc  35401  dmopab3rexdif  35441  cbvabdavw  36290  neifg  36405  filnetlem4  36415  ontgval  36465  bj-gabima  36974  bj-restsn  37116  bj-rest10  37122  bj-restpw  37126  bj-restuni  37131  mptsnunlem  37372  finxpsuclem  37431  wl-clabtv  37631  wl-clabt  37632  poimirlem16  37676  poimirlem19  37679  poimirlem23  37683  poimirlem27  37687  heicant  37695  istotbnd3  37811  sstotbnd  37815  ismtyima  37843  heibor  37861  divrngidl  38068  eccnvep  38316  ecxrn  38419  eqvrelth  38648  disjlem19  38839  prtlem19  38917  prter2  38920  lkrsc  39136  lshpkr  39156  paddvaln0N  39840  paddval0  39849  diaglbN  41094  cdlemm10N  41157  lcfrvalsnN  41580  lcfrlem9  41589  lcdlss  41658  mapd1o  41687  mapd0  41704  hlhillcs  41997  grpods  42227  unitscyglem2  42229  sn-iotalem  42254  fsuppind  42623  mzpmfp  42780  lzunuz  42801  fz1eqin  42802  jm2.23  43029  pw2f1ocnv  43070  dfacbasgrp  43141  nnoeomeqom  43345  oadif1lem  43412  oadif1  43413  fzunt  43488  fzuntd  43489  fzunt1d  43490  fzuntgd  43491  inintabd  43612  cnvcnvintabd  43633  cnvintabd  43636  rfcnpre3  45070  rfcnpre4  45071  iindif2f  45197  rnmptpr  45214  iccshift  45558  iocopn  45560  iooshift  45562  iccintsng  45563  icoopn  45565  limcdm0  45658  limcresiooub  45680  limcresioolb  45681  fperdvper  45957  itgperiod  46019  fourierdlem32  46177  fourierdlem33  46178  fourierdlem48  46192  fourierdlem49  46193  fourierdlem81  46225  fsetsniunop  47080  elsetpreimafvrab  47425  iccpartiun  47465  dfclnbgr6  47887  dfnbgr6  47888  uhgrimisgrgric  47962  clnbgrgrim  47965  stgredgiun  47989  gpgnbgrvtx0  48105  gpgnbgrvtx1  48106  itsclinecirc0in  48807  i0oii  48951  io1ii  48952  sectpropd  49069  invpropd  49071  isopropd  49073  cicpropd  49082  uobffth  49250  uobeqw  49251  natoppfb  49263  oppc1stflem  49319  thincmon  49465  thincepi  49466  termfucterm  49576  grptcmon  49625  grptcepi  49626  lanval2  49659  ranval2  49662  ranval3  49663