Theorem eqrdv 2735

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

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

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqrdav  2736  abbi  2807  eqabdv  2875  uneq1  4161  unineq  4288  difin2  4301  difsn  4798  eqsndOLD  4831  intmin4  4977  iunconst  5001  iinconst  5002  iuneqconst  5003  dfiun2g  5030  dfiun2gOLD  5031  iindif1  5075  iindif2  5077  iinin2  5078  iunxsng  5090  iunxsngf  5092  opthprc  5749  dmopab2rex  5928  dmxp  5939  epin  6113  inimasn  6176  dmsnopg  6233  dfco2a  6266  iotaeq  6526  imadif  6650  unima  6984  ssimaex  6994  unpreima  7083  respreima  7086  iinpreima  7089  fnsnb  7186  fmptsng  7188  fmptsnd  7189  tpres  7221  iunpw  7791  ordpwsuc  7835  ordsucun  7845  fiun  7967  f1iun  7968  reldm  8069  fimaproj  8160  xpord2pred  8170  xpord3pred  8177  rntpos  8264  onoviun  8383  oarec  8600  iserd  8771  erth  8796  mapdm0  8882  mapfset  8890  ixpiin  8964  boxriin  8980  pw2f1olem  9116  fifo  9472  ordiso2  9555  ttrclse  9767  finacn  10090  acnen  10093  acacni  10181  dfac13  10183  fin23lem26  10365  isf34lem4  10417  axdc3lem2  10491  fpwwe2lem7  10677  fpwwe2lem11  10681  fpwwe2lem12  10682  gch2  10715  gchac  10721  gchina  10739  genpass  11049  1idpr  11069  eqreznegel  12976  ixxun  13403  iccid  13432  difreicc  13524  iccsplit  13525  fzsplit2  13589  fzsn  13606  fzpr  13619  uzsplit  13636  fzdif1  13645  preduz  13690  predfz  13693  fz1isolem  14500  pr2pwpr  14518  isercolllem2  15702  isercoll  15704  bitsmod  16473  bitscmp  16475  saddisj  16502  sadadd  16504  sadass  16508  smupvallem  16520  smueqlem  16527  smumul  16530  gcdcllem2  16537  vdwapun  17012  firest  17477  fncnvimaeqv  18164  mgmhmpropd  18711  mhmpropd  18805  efmnd1bas  18906  subgacs  19179  eqgid  19198  ghmmhmb  19245  ghmpropd  19274  ghmqusnsglem1  19298  ghmquskerlem1  19301  ghmqusker  19305  resscntz  19351  symg1bas  19408  lsmcom2  19673  lsmass  19687  ablnsg  19865  lsmcomx  19874  gsum2d2  19992  subgdmdprd  20054  dprd2d2  20064  2nsgsimpgd  20122  unitpropd  20417  rnghmval2  20444  subsubrng2  20564  subrngpropd  20568  subsubrg2  20599  subrgpropd  20608  rhmpropd  20609  subrgacs  20801  sdrgacs  20802  abvpropd  20836  lssacs  20965  lssats2  20998  lsspropd  21016  lmhmpropd  21072  lbspropd  21098  pzriprnglem10  21501  psdmul  22170  discld  23097  neiptopnei  23140  neiptopreu  23141  restsn  23178  restdis  23186  neitr  23188  restlp  23191  cndis  23299  cnindis  23300  cnpdis  23301  lpcls  23372  hausmapdom  23508  ptpjpre1  23579  tx1cn  23617  tx2cn  23618  hauseqlcld  23654  txkgen  23660  idqtop  23714  tgqtop  23720  acufl  23925  uffix  23929  ufildr  23939  fmfg  23957  rnelfm  23961  fmfnfm  23966  fmid  23968  fmco  23969  flimrest  23991  fclsrest  24032  alexsubALT  24059  tsmsgsum  24147  tsmssubm  24151  tsmsres  24152  tsmsf1o  24153  xpsdsval  24391  blpnf  24407  blin  24431  blres  24441  xmetec  24444  imasf1obl  24501  imasf1oxms  24502  prdsbl  24504  metrest  24537  psmetutop  24580  restmetu  24583  dscopn  24586  cnbl0  24794  bl2ioo  24813  xrtgioo  24828  cncfmet  24935  icoopnst  24969  iocopnst  24970  cldcss2  25476  iunmbl2  25592  mbfmulc2lem  25682  mbfmax  25684  ismbf3d  25689  mbfimaopnlem  25690  mbfaddlem  25695  mbfsup  25699  i1f1lem  25724  i1faddlem  25728  i1fmullem  25729  i1fmulclem  25737  i1fres  25740  mbfi1fseqlem4  25753  limcdif  25911  limcnlp  25913  limcflf  25916  limcres  25921  limcun  25930  ply1remlem  26204  fta1glem2  26208  plypf1  26251  ofmulrt  26323  plyremlem  26346  aannenlem1  26370  gausslemma2dlem1a  27409  oldlim  27925  tglineelsb2  28640  tglinecom  28643  ushgredgedg  29246  ushgredgedgloop  29248  nbumgrvtx  29363  nbusgrvtxm1uvtx  29422  vdiscusgr  29549  wspniunwspnon  29943  rusgrnumwwlkb0  29991  clwwlknscsh  30081  clwwlknun  30131  eupth2lems  30257  fusgr2wsp2nb  30353  fusgreg2wsp  30355  ubthlem1  30889  ocin  31315  shscom  31338  spansncol  31587  iunsnima  32630  iunsnima2  32631  nfpconfp  32642  unipreima  32653  2ndimaxp  32656  fdifsupp  32694  suppiniseg  32695  ressupprn  32699  1stpreimas  32715  1stpreima  32716  2ndpreima  32717  fpwrelmapffslem  32743  iocinioc2  32781  nndiffz1  32788  fzsplit3  32795  indpi1  32845  indf1ofs  32851  swrdrn3  32940  cntzun  33071  cntzsnid  33072  ecxpid  33389  qsxpid  33390  lindspropd  33411  lsmsnpridl  33426  lsmssass  33430  grplsm0l  33431  grplsmid  33432  nsgqusf1olem2  33442  nsgqusf1olem3  33443  crngmxidl  33497  opprlidlabs  33513  rprmirredb  33560  ressply1mon1p  33593  fldextrspunlsp  33724  irngnzply1  33741  smatrcl  33795  qtophaus  33835  locfinreflem  33839  rspectopn  33866  zarclsiin  33870  rhmpreimacnlem  33883  prsdm  33913  prsrn  33914  1stmbfm  34262  2ndmbfm  34263  mbfmcnt  34270  eulerpartlemgh  34380  dstfrvunirn  34477  reprsuc  34630  reprpmtf1o  34641  satfvsucsuc  35370  dmopab3rexdif  35410  cbvabdavw  36257  neifg  36372  filnetlem4  36382  ontgval  36432  bj-gabima  36941  bj-restsn  37083  bj-rest10  37089  bj-restpw  37093  bj-restuni  37098  mptsnunlem  37339  finxpsuclem  37398  wl-clabtv  37598  wl-clabt  37599  poimirlem16  37643  poimirlem19  37646  poimirlem23  37650  poimirlem27  37654  heicant  37662  istotbnd3  37778  sstotbnd  37782  ismtyima  37810  heibor  37828  divrngidl  38035  eccnvep  38283  ecxrn  38388  eqvrelth  38612  disjlem19  38802  prtlem19  38879  prter2  38882  lkrsc  39098  lshpkr  39118  paddvaln0N  39803  paddval0  39812  diaglbN  41057  cdlemm10N  41120  lcfrvalsnN  41543  lcfrlem9  41552  lcdlss  41621  mapd1o  41650  mapd0  41667  hlhillcs  41964  grpods  42195  unitscyglem2  42197  sn-iotalem  42260  fnsnbt  42271  fsuppind  42600  mzpmfp  42758  lzunuz  42779  fz1eqin  42780  jm2.23  43008  pw2f1ocnv  43049  dfacbasgrp  43120  nnoeomeqom  43325  oadif1lem  43392  oadif1  43393  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  inintabd  43592  cnvcnvintabd  43613  cnvintabd  43616  rfcnpre3  45038  rfcnpre4  45039  iindif2f  45165  rnmptpr  45182  iccshift  45531  iocopn  45533  iooshift  45535  iccintsng  45536  icoopn  45538  limcdm0  45633  limcresiooub  45657  limcresioolb  45658  fperdvper  45934  itgperiod  45996  fourierdlem32  46154  fourierdlem33  46155  fourierdlem48  46169  fourierdlem49  46170  fourierdlem81  46202  fsetsniunop  47061  elsetpreimafvrab  47381  iccpartiun  47421  dfclnbgr6  47842  dfnbgr6  47843  uhgrimisgrgric  47899  clnbgrgrim  47902  stgredgiun  47925  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  itsclinecirc0in  48696  i0oii  48817  io1ii  48818  thincmon  49082  thincepi  49083  grptcmon  49190  grptcepi  49191