Theorem eqrdv 2608

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

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  eqrdav  2609  uneq1  3722  ineq1  3769  unineq  3836  difin2  3849  difsn  4269  intmin4  4441  iunconst  4465  iinconst  4466  dfiun2g  4488  iindif2  4525  iinin2  4526  iunxsng  4538  opthprc  5089  inimasn  5469  dmsnopg  5524  dfco2a  5552  iotaeq  5776  imadif  5887  ssimaex  6173  unpreima  6249  respreima  6252  iinpreima  6253  fnsnb  6337  fmptsng  6339  fmptsnd  6340  tpres  6371  iunpw  6870  ordpwsuc  6907  ordsucun  6917  fun11iun  7019  reldm  7110  rntpos  7252  onoviun  7327  oarec  7529  iserd  7655  erth  7678  map0e  7781  ixpiin  7820  boxriin  7836  pw2f1olem  7949  fifo  8221  ordiso2  8303  finacn  8756  acnen  8759  acacni  8845  dfac13  8847  fin23lem26  9030  isf34lem4  9082  axdc3lem2  9156  fpwwe2lem8  9338  fpwwe2lem12  9342  fpwwe2lem13  9343  gch2  9376  gchac  9382  gchina  9400  genpass  9710  1idpr  9730  eqreznegel  11650  ixxun  12062  iccid  12091  difreicc  12175  iccsplit  12176  fzsplit2  12237  fzsn  12254  fzpr  12266  uzsplit  12281  preduz  12330  predfz  12333  fz1isolem  13102  pr2pwpr  13116  isercolllem2  14244  isercoll  14246  bitsmod  14996  bitscmp  14998  saddisj  15025  sadadd  15027  sadass  15031  smupvallem  15043  smueqlem  15050  smumul  15053  gcdcllem2  15060  vdwapun  15516  firest  15916  fncnvimaeqv  16583  mhmpropd  17164  subgacs  17452  eqgid  17469  ghmmhmb  17494  ghmpropd  17521  resscntz  17587  symg1bas  17639  lsmcom2  17893  lsmass  17906  ablnsg  18073  lsmcomx  18082  gsum2d2  18196  subgdmdprd  18256  dprd2d2  18266  unitpropd  18520  subsubrg2  18630  subrgpropd  18637  rhmpropd  18638  abvpropd  18665  lssacs  18788  lssats2  18821  lsspropd  18838  lmhmpropd  18894  lbspropd  18920  discld  20703  neiptopnei  20746  neiptopreu  20747  restsn  20784  restdis  20792  neitr  20794  restlp  20797  cndis  20905  cnindis  20906  cnpdis  20907  lpcls  20978  hausmapdom  21113  ptpjpre1  21184  tx1cn  21222  tx2cn  21223  hauseqlcld  21259  txkgen  21265  idqtop  21319  tgqtop  21325  acufl  21531  uffix  21535  ufildr  21545  fmfg  21563  rnelfm  21567  fmfnfm  21572  fmid  21574  fmco  21575  flimrest  21597  fclsrest  21638  alexsubALT  21665  tsmsgsum  21752  tsmssubm  21756  tsmsres  21757  tsmsf1o  21758  xpsdsval  21996  blpnf  22012  blin  22036  blres  22046  xmetec  22049  imasf1obl  22103  imasf1oxms  22104  prdsbl  22106  metrest  22139  psmetutop  22182  restmetu  22185  dscopn  22188  cnbl0  22387  bl2ioo  22403  xrtgioo  22417  cncfmet  22519  icoopnst  22546  iocopnst  22547  cldcss2  23021  iunmbl2  23132  mbfmulc2lem  23220  mbfmax  23222  ismbf3d  23227  mbfimaopnlem  23228  mbfaddlem  23233  mbfsup  23237  i1f1lem  23262  i1faddlem  23266  i1fmullem  23267  i1fmulclem  23275  i1fres  23278  mbfi1fseqlem4  23291  limcdif  23446  limcnlp  23448  limcflf  23451  limcres  23456  limcun  23465  ply1remlem  23726  fta1glem2  23730  plypf1  23772  ofmulrt  23841  plyremlem  23863  aannenlem1  23887  gausslemma2dlem1a  24890  tglineelsb2  25327  tglinecom  25330  cusgrarn  25988  uvtxnbgra  26021  clwwlknscsh  26347  2wot2wont  26413  2spot2iun2spont  26418  nbhashuvtx  26443  vdiscusgra  26448  rusgranumwlkb0  26480  eupath2  26507  usg2spot2nb  26592  usgreg2spot  26594  numclwwlkun  26606  ubthlem1  27110  ocin  27539  shscom  27562  spansncol  27811  iunxsngf  28758  iunsnima  28808  unipreima  28826  1stpreimas  28866  1stpreima  28867  2ndpreima  28868  fpwrelmapffslem  28895  iocinioc2  28931  nndiffz1  28936  fzsplit3  28940  smatrcl  29190  fimaproj  29228  qtophaus  29231  locfinreflem  29235  prsdm  29288  prsrn  29289  indpi1  29411  indf1ofs  29415  1stmbfm  29649  2ndmbfm  29650  mbfmcnt  29657  eulerpartlemgh  29767  dstfrvunirn  29863  neifg  31536  filnetlem4  31546  ontgval  31600  bj-restsn  32216  bj-rest10  32222  bj-restpw  32226  bj-restuni  32231  mptsnunlem  32361  finxpsuclem  32410  poimirlem16  32595  poimirlem19  32598  poimirlem23  32602  poimirlem27  32606  heicant  32614  istotbnd3  32740  sstotbnd  32744  ismtyima  32772  heibor  32790  divrngidl  32997  prtlem19  33181  prter2  33184  lkrsc  33402  lshpkr  33422  paddvaln0N  34105  paddval0  34114  diaglbN  35362  cdlemm10N  35425  lcfrvalsnN  35848  lcfrlem9  35857  lcdlss  35926  mapd1o  35955  mapd0  35972  hlhillcs  36268  mzpmfp  36328  lzunuz  36349  fz1eqin  36350  jm2.23  36581  pw2f1ocnv  36622  dfacbasgrp  36697  subrgacs  36789  sdrgacs  36790  inintabd  36904  cnvcnvintabd  36925  cnvintabd  36928  csbabgOLD  38072  rfcnpre3  38215  rfcnpre4  38216  iunxsngf2  38255  unima  38340  iccshift  38591  iocopn  38593  iooshift  38595  iccintsng  38596  icoopn  38598  limcdm0  38685  limcresiooub  38709  limcresioolb  38710  fperdvper  38808  itgperiod  38873  fourierdlem32  39032  fourierdlem33  39033  fourierdlem48  39047  fourierdlem49  39048  fourierdlem81  39080  iccpartiun  39972  ushgredgedga  40456  ushgredgedgaloop  40458  nbumgrvtx  40568  nbusgrvtxm1uvtx  40632  vdiscusgr  40747  wspniunwspnon  41130  rusgrnumwwlkb0  41174  clwwlksnscsh  41247  clwwlksnun  41281  eupth2lems  41406  fusgr2wsp2nb  41498  fusgreg2wsp  41500  mgmhmpropd  41575  rnghmval2  41685