Theorem eqrdv 2727

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eqrdav  2728  abbi  2794  eqabdv  2861  uneq1  4120  unineq  4247  difin2  4260  difsn  4758  eqsndOLD  4791  intmin4  4937  iunconst  4961  iinconst  4962  iuneqconst  4963  dfiun2g  4990  iindif1  5034  iindif2  5036  iinin2  5037  iunxsng  5049  iunxsngf  5051  opthprc  5695  dmopab2rex  5871  dmxp  5882  epin  6055  inimasn  6117  dmsnopg  6174  dfco2a  6207  iotaeq  6464  imadif  6584  unima  6918  ssimaex  6928  unpreima  7017  respreima  7020  iinpreima  7023  fnsnbg  7120  fnsnbOLD  7122  fmptsng  7124  fmptsnd  7125  tpres  7157  iunpw  7727  ordpwsuc  7770  ordsucun  7780  fiun  7901  f1iun  7902  reldm  8002  fimaproj  8091  xpord2pred  8101  xpord3pred  8108  rntpos  8195  onoviun  8289  oarec  8503  iserd  8674  erth  8702  mapdm0  8792  mapfset  8800  ixpiin  8874  boxriin  8890  pw2f1olem  9022  fifo  9359  ordiso2  9444  ttrclse  9656  finacn  9979  acnen  9982  acacni  10070  dfac13  10072  fin23lem26  10254  isf34lem4  10306  axdc3lem2  10380  fpwwe2lem7  10566  fpwwe2lem11  10570  fpwwe2lem12  10571  gch2  10604  gchac  10610  gchina  10628  genpass  10938  1idpr  10958  eqreznegel  12869  ixxun  13298  iccid  13327  difreicc  13421  iccsplit  13422  fzsplit2  13486  fzsn  13503  fzpr  13516  uzsplit  13533  fzdif1  13542  preduz  13587  predfz  13590  fz1isolem  14402  pr2pwpr  14420  isercolllem2  15608  isercoll  15610  bitsmod  16382  bitscmp  16384  saddisj  16411  sadadd  16413  sadass  16417  smupvallem  16429  smueqlem  16436  smumul  16439  gcdcllem2  16446  vdwapun  16921  firest  17371  fncnvimaeqv  18057  mgmhmpropd  18601  mhmpropd  18695  efmnd1bas  18796  subgacs  19069  eqgid  19088  ghmmhmb  19135  ghmpropd  19164  ghmqusnsglem1  19188  ghmquskerlem1  19191  ghmqusker  19195  resscntz  19241  symg1bas  19297  lsmcom2  19561  lsmass  19575  ablnsg  19753  lsmcomx  19762  gsum2d2  19880  subgdmdprd  19942  dprd2d2  19952  2nsgsimpgd  20010  unitpropd  20302  rnghmval2  20329  subsubrng2  20449  subrngpropd  20453  subsubrg2  20484  subrgpropd  20493  rhmpropd  20494  subrgacs  20685  sdrgacs  20686  abvpropd  20720  lssacs  20849  lssats2  20882  lsspropd  20900  lmhmpropd  20956  lbspropd  20982  pzriprnglem10  21376  psdmul  22029  discld  22952  neiptopnei  22995  neiptopreu  22996  restsn  23033  restdis  23041  neitr  23043  restlp  23046  cndis  23154  cnindis  23155  cnpdis  23156  lpcls  23227  hausmapdom  23363  ptpjpre1  23434  tx1cn  23472  tx2cn  23473  hauseqlcld  23509  txkgen  23515  idqtop  23569  tgqtop  23575  acufl  23780  uffix  23784  ufildr  23794  fmfg  23812  rnelfm  23816  fmfnfm  23821  fmid  23823  fmco  23824  flimrest  23846  fclsrest  23887  alexsubALT  23914  tsmsgsum  24002  tsmssubm  24006  tsmsres  24007  tsmsf1o  24008  xpsdsval  24245  blpnf  24261  blin  24285  blres  24295  xmetec  24298  imasf1obl  24352  imasf1oxms  24353  prdsbl  24355  metrest  24388  psmetutop  24431  restmetu  24434  dscopn  24437  cnbl0  24637  bl2ioo  24656  xrtgioo  24671  cncfmet  24778  icoopnst  24812  iocopnst  24813  cldcss2  25318  iunmbl2  25434  mbfmulc2lem  25524  mbfmax  25526  ismbf3d  25531  mbfimaopnlem  25532  mbfaddlem  25537  mbfsup  25541  i1f1lem  25566  i1faddlem  25570  i1fmullem  25571  i1fmulclem  25579  i1fres  25582  mbfi1fseqlem4  25595  limcdif  25753  limcnlp  25755  limcflf  25758  limcres  25763  limcun  25772  ply1remlem  26046  fta1glem2  26050  plypf1  26093  ofmulrt  26165  plyremlem  26188  aannenlem1  26212  gausslemma2dlem1a  27252  oldlim  27774  tglineelsb2  28535  tglinecom  28538  ushgredgedg  29132  ushgredgedgloop  29134  nbumgrvtx  29249  nbusgrvtxm1uvtx  29308  vdiscusgr  29435  wspniunwspnon  29826  rusgrnumwwlkb0  29874  clwwlknscsh  29964  clwwlknun  30014  eupth2lems  30140  fusgr2wsp2nb  30236  fusgreg2wsp  30238  ubthlem1  30772  ocin  31198  shscom  31221  spansncol  31470  iunsnima  32519  iunsnima2  32520  nfpconfp  32529  unipreima  32540  2ndimaxp  32543  fdifsupp  32581  suppiniseg  32582  ressupprn  32586  1stpreimas  32602  1stpreima  32603  2ndpreima  32604  fpwrelmapffslem  32628  iocinioc2  32675  nndiffz1  32682  fzsplit3  32689  indpi1  32756  indf1ofs  32762  swrdrn3  32850  cntzun  32981  cntzsnid  32982  cntrval2  33101  ecxpid  33305  qsxpid  33306  lindspropd  33327  lsmsnpridl  33342  lsmssass  33346  grplsm0l  33347  grplsmid  33348  nsgqusf1olem2  33358  nsgqusf1olem3  33359  crngmxidl  33413  opprlidlabs  33429  rprmirredb  33476  ressply1mon1p  33510  fldextrspunlsp  33642  irngnzply1  33659  smatrcl  33759  qtophaus  33799  locfinreflem  33803  rspectopn  33830  zarclsiin  33834  rhmpreimacnlem  33847  prsdm  33877  prsrn  33878  1stmbfm  34224  2ndmbfm  34225  mbfmcnt  34232  eulerpartlemgh  34342  dstfrvunirn  34439  reprsuc  34579  reprpmtf1o  34590  satfvsucsuc  35325  dmopab3rexdif  35365  cbvabdavw  36217  neifg  36332  filnetlem4  36342  ontgval  36392  bj-gabima  36901  bj-restsn  37043  bj-rest10  37049  bj-restpw  37053  bj-restuni  37058  mptsnunlem  37299  finxpsuclem  37358  wl-clabtv  37558  wl-clabt  37559  poimirlem16  37603  poimirlem19  37606  poimirlem23  37610  poimirlem27  37614  heicant  37622  istotbnd3  37738  sstotbnd  37742  ismtyima  37770  heibor  37788  divrngidl  37995  eccnvep  38243  ecxrn  38346  eqvrelth  38575  disjlem19  38766  prtlem19  38844  prter2  38847  lkrsc  39063  lshpkr  39083  paddvaln0N  39768  paddval0  39777  diaglbN  41022  cdlemm10N  41085  lcfrvalsnN  41508  lcfrlem9  41517  lcdlss  41586  mapd1o  41615  mapd0  41632  hlhillcs  41925  grpods  42155  unitscyglem2  42157  sn-iotalem  42182  fsuppind  42551  mzpmfp  42708  lzunuz  42729  fz1eqin  42730  jm2.23  42958  pw2f1ocnv  42999  dfacbasgrp  43070  nnoeomeqom  43274  oadif1lem  43341  oadif1  43342  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  inintabd  43541  cnvcnvintabd  43562  cnvintabd  43565  rfcnpre3  45000  rfcnpre4  45001  iindif2f  45127  rnmptpr  45144  iccshift  45489  iocopn  45491  iooshift  45493  iccintsng  45494  icoopn  45496  limcdm0  45589  limcresiooub  45613  limcresioolb  45614  fperdvper  45890  itgperiod  45952  fourierdlem32  46110  fourierdlem33  46111  fourierdlem48  46125  fourierdlem49  46126  fourierdlem81  46158  fsetsniunop  47023  elsetpreimafvrab  47368  iccpartiun  47408  dfclnbgr6  47829  dfnbgr6  47830  uhgrimisgrgric  47904  clnbgrgrim  47907  stgredgiun  47930  gpgnbgrvtx0  48038  gpgnbgrvtx1  48039  itsclinecirc0in  48737  i0oii  48881  io1ii  48882  sectpropd  48999  invpropd  49001  isopropd  49003  cicpropd  49012  uobffth  49180  uobeqw  49181  natoppfb  49193  oppc1stflem  49249  thincmon  49395  thincepi  49396  termfucterm  49506  grptcmon  49555  grptcepi  49556  lanval2  49589  ranval2  49592  ranval3  49593