Theorem eqrdv 2734

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  eqrdav  2735  abbi  2801  eqabdv  2869  uneq1  4101  unineq  4228  difin2  4241  difsn  4743  eqsndOLD  4774  intmin4  4919  intprg  4923  iunconst  4943  iinconst  4944  iuneqconst  4945  dfiun2g  4972  iindif1  5017  iindif2  5019  iinin2  5020  iunxsng  5032  iunxsngf  5034  opthprc  5695  dmopab2rex  5872  dmxp  5884  epin  6060  inimasn  6120  dmsnopg  6177  dfco2a  6210  iotaeq  6466  imadif  6582  unima  6915  ssimaex  6925  unpreima  7015  respreima  7018  iinpreima  7021  fnsnbg  7119  fnsnbOLD  7121  fmptsng  7123  fmptsnd  7124  tpres  7156  iunpw  7725  ordpwsuc  7766  ordsucun  7776  fiun  7896  f1iun  7897  reldm  7997  fimaproj  8085  xpord2pred  8095  xpord3pred  8102  rntpos  8189  onoviun  8283  oarec  8497  iserd  8670  erth  8698  mapdm0  8789  mapfset  8797  ixpiin  8872  boxriin  8888  pw2f1olem  9019  fifo  9345  ordiso2  9430  ttrclse  9648  finacn  9972  acnen  9975  acacni  10063  dfac13  10065  fin23lem26  10247  isf34lem4  10299  axdc3lem2  10373  fpwwe2lem7  10560  fpwwe2lem11  10564  fpwwe2lem12  10565  gch2  10598  gchac  10604  gchina  10622  genpass  10932  1idpr  10952  indpi1  12173  eqreznegel  12884  ixxun  13314  iccid  13343  difreicc  13437  iccsplit  13438  fzsplit2  13503  fzsn  13520  fzpr  13533  uzsplit  13550  fzdif1  13559  preduz  13604  predfz  13607  fz1isolem  14423  pr2pwpr  14441  isercolllem2  15628  isercoll  15630  bitsmod  16405  bitscmp  16407  saddisj  16434  sadadd  16436  sadass  16440  smupvallem  16452  smueqlem  16459  smumul  16462  gcdcllem2  16469  vdwapun  16945  firest  17395  fncnvimaeqv  18086  mgmhmpropd  18666  mhmpropd  18760  efmnd1bas  18861  subgacs  19136  eqgid  19155  ghmmhmb  19202  ghmpropd  19231  ghmqusnsglem1  19255  ghmquskerlem1  19258  ghmqusker  19262  resscntz  19308  symg1bas  19366  lsmcom2  19630  lsmass  19644  ablnsg  19822  lsmcomx  19831  gsum2d2  19949  subgdmdprd  20011  dprd2d2  20021  2nsgsimpgd  20079  unitpropd  20397  rnghmval2  20424  subsubrng2  20541  subrngpropd  20545  subsubrg2  20576  subrgpropd  20585  rhmpropd  20586  subrgacs  20777  sdrgacs  20778  abvpropd  20812  lssacs  20962  lssats2  20995  lsspropd  21012  lmhmpropd  21068  lbspropd  21094  pzriprnglem10  21470  psdmul  22132  discld  23054  neiptopnei  23097  neiptopreu  23098  restsn  23135  restdis  23143  neitr  23145  restlp  23148  cndis  23256  cnindis  23257  cnpdis  23258  lpcls  23329  hausmapdom  23465  ptpjpre1  23536  tx1cn  23574  tx2cn  23575  hauseqlcld  23611  txkgen  23617  idqtop  23671  tgqtop  23677  acufl  23882  uffix  23886  ufildr  23896  fmfg  23914  rnelfm  23918  fmfnfm  23923  fmid  23925  fmco  23926  flimrest  23948  fclsrest  23989  alexsubALT  24016  tsmsgsum  24104  tsmssubm  24108  tsmsres  24109  tsmsf1o  24110  xpsdsval  24346  blpnf  24362  blin  24386  blres  24396  xmetec  24399  imasf1obl  24453  imasf1oxms  24454  prdsbl  24456  metrest  24489  psmetutop  24532  restmetu  24535  dscopn  24538  cnbl0  24738  bl2ioo  24757  xrtgioo  24772  cncfmet  24876  icoopnst  24906  iocopnst  24907  cldcss2  25409  iunmbl2  25524  mbfmulc2lem  25614  mbfmax  25616  ismbf3d  25621  mbfimaopnlem  25622  mbfaddlem  25627  mbfsup  25631  i1f1lem  25656  i1faddlem  25660  i1fmullem  25661  i1fmulclem  25669  i1fres  25672  mbfi1fseqlem4  25685  limcdif  25843  limcnlp  25845  limcflf  25848  limcres  25853  limcun  25862  ply1remlem  26130  fta1glem2  26134  plypf1  26177  ofmulrt  26248  plyremlem  26270  aannenlem1  26294  gausslemma2dlem1a  27328  oldlim  27879  negleft  28050  negright  28051  tglineelsb2  28700  tglinecom  28703  ushgredgedg  29298  ushgredgedgloop  29300  nbumgrvtx  29415  nbusgrvtxm1uvtx  29474  vdiscusgr  29600  wspniunwspnon  29991  rusgrnumwwlkb0  30042  clwwlknscsh  30132  clwwlknun  30182  eupth2lems  30308  fusgr2wsp2nb  30404  fusgreg2wsp  30406  ubthlem1  30941  ocin  31367  shscom  31390  spansncol  31639  iunsnima  32691  iunsnima2  32692  nfpconfp  32705  unipreima  32716  2ndimaxp  32719  fdifsupp  32758  suppiniseg  32759  ressupprn  32763  1stpreimas  32779  1stpreima  32780  2ndpreima  32781  fpwrelmapffslem  32805  iocinioc2  32852  nndiffz1  32859  fzsplit3  32866  indf1ofs  32926  swrdrn3  33015  cntzun  33140  cntzsnid  33141  cntrval2  33232  ecxpid  33421  qsxpid  33422  lindspropd  33443  lsmsnpridl  33458  lsmssass  33462  grplsm0l  33463  grplsmid  33464  nsgqusf1olem2  33474  nsgqusf1olem3  33475  crngmxidl  33529  opprlidlabs  33545  rprmirredb  33592  ressply1mon1p  33628  fldextrspunlsp  33818  irngnzply1  33835  smatrcl  33940  qtophaus  33980  locfinreflem  33984  rspectopn  34011  zarclsiin  34015  rhmpreimacnlem  34028  prsdm  34058  prsrn  34059  1stmbfm  34404  2ndmbfm  34405  mbfmcnt  34412  eulerpartlemgh  34522  dstfrvunirn  34619  reprsuc  34759  reprpmtf1o  34770  satfvsucsuc  35547  dmopab3rexdif  35587  cbvabdavw  36438  neifg  36553  filnetlem4  36563  ontgval  36613  bj-gabima  37247  bj-restsn  37394  bj-rest10  37400  bj-restpw  37404  bj-restuni  37409  mptsnunlem  37654  finxpsuclem  37713  wl-clabtv  37911  wl-clabt  37912  poimirlem16  37957  poimirlem19  37960  poimirlem23  37964  poimirlem27  37968  heicant  37976  istotbnd3  38092  sstotbnd  38096  ismtyima  38124  heibor  38142  divrngidl  38349  eccnvep  38609  ecxrn  38727  eqvrelth  39016  disjlem19  39225  prtlem19  39324  prter2  39327  lkrsc  39543  lshpkr  39563  paddvaln0N  40247  paddval0  40256  diaglbN  41501  cdlemm10N  41564  lcfrvalsnN  41987  lcfrlem9  41996  lcdlss  42065  mapd1o  42094  mapd0  42111  hlhillcs  42404  grpods  42633  unitscyglem2  42635  sn-iotalem  42662  fsuppind  43023  mzpmfp  43179  lzunuz  43200  fz1eqin  43201  jm2.23  43424  pw2f1ocnv  43465  dfacbasgrp  43536  nnoeomeqom  43740  oadif1lem  43807  oadif1  43808  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  inintabd  44006  cnvcnvintabd  44027  cnvintabd  44030  rfcnpre3  45464  rfcnpre4  45465  iindif2f  45590  rnmptpr  45607  iccshift  45948  iocopn  45950  iooshift  45952  iccintsng  45953  icoopn  45955  limcdm0  46048  limcresiooub  46070  limcresioolb  46071  fperdvper  46347  itgperiod  46409  fourierdlem32  46567  fourierdlem33  46568  fourierdlem48  46582  fourierdlem49  46583  fourierdlem81  46615  fsetsniunop  47497  elsetpreimafvrab  47854  iccpartiun  47894  dfclnbgr6  48332  dfnbgr6  48333  uhgrimisgrgric  48407  clnbgrgrim  48410  stgredgiun  48434  gpgnbgrvtx0  48550  gpgnbgrvtx1  48551  itsclinecirc0in  49251  i0oii  49395  io1ii  49396  sectpropd  49512  invpropd  49514  isopropd  49516  cicpropd  49525  uobffth  49693  uobeqw  49694  natoppfb  49706  oppc1stflem  49762  thincmon  49908  thincepi  49909  termfucterm  50019  grptcmon  50068  grptcepi  50069  lanval2  50102  ranval2  50105  ranval3  50106