Theorem eqrdv 2731

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  eqrdav  2732  abbi  2801  eqabdv  2868  ss2abdv  4060  uneq1  4156  unineq  4277  difin2  4291  difsn  4801  intmin4  4981  iunconst  5006  iinconst  5007  iuneqconst  5008  dfiun2g  5033  dfiun2gOLD  5034  iindif1  5078  iindif2  5080  iinin2  5081  iunxsng  5093  iunxsngf  5095  opthprc  5739  dmopab2rex  5916  epin  6092  inimasn  6153  dmsnopg  6210  dfco2a  6243  iotaeq  6506  imadif  6630  unima  6964  ssimaex  6974  unpreima  7062  respreima  7065  iinpreima  7068  fnsnb  7161  fmptsng  7163  fmptsnd  7164  tpres  7199  iunpw  7755  ordpwsuc  7800  ordsucun  7810  fiun  7926  f1iun  7927  reldm  8027  fimaproj  8118  xpord2pred  8128  xpord3pred  8135  rntpos  8221  onoviun  8340  oarec  8559  iserd  8726  erth  8749  mapdm0  8833  mapfset  8841  ixpiin  8915  boxriin  8931  pw2f1olem  9073  fifo  9424  ordiso2  9507  ttrclse  9719  finacn  10042  acnen  10045  acacni  10132  dfac13  10134  fin23lem26  10317  isf34lem4  10369  axdc3lem2  10443  fpwwe2lem7  10629  fpwwe2lem11  10633  fpwwe2lem12  10634  gch2  10667  gchac  10673  gchina  10691  genpass  11001  1idpr  11021  eqreznegel  12915  ixxun  13337  iccid  13366  difreicc  13458  iccsplit  13459  fzsplit2  13523  fzsn  13540  fzpr  13553  uzsplit  13570  preduz  13620  predfz  13623  fz1isolem  14419  pr2pwpr  14437  isercolllem2  15609  isercoll  15611  bitsmod  16374  bitscmp  16376  saddisj  16403  sadadd  16405  sadass  16409  smupvallem  16421  smueqlem  16428  smumul  16431  gcdcllem2  16438  vdwapun  16904  firest  17375  fncnvimaeqv  18068  mhmpropd  18675  efmnd1bas  18771  subgacs  19036  eqgid  19055  ghmmhmb  19098  ghmpropd  19125  resscntz  19192  symg1bas  19253  lsmcom2  19518  lsmass  19532  ablnsg  19710  lsmcomx  19719  gsum2d2  19837  subgdmdprd  19899  dprd2d2  19909  2nsgsimpgd  19967  unitpropd  20224  subsubrg2  20384  subrgpropd  20393  rhmpropd  20394  subrgacs  20409  sdrgacs  20410  abvpropd  20443  lssacs  20571  lssats2  20604  lsspropd  20621  lmhmpropd  20677  lbspropd  20703  discld  22585  neiptopnei  22628  neiptopreu  22629  restsn  22666  restdis  22674  neitr  22676  restlp  22679  cndis  22787  cnindis  22788  cnpdis  22789  lpcls  22860  hausmapdom  22996  ptpjpre1  23067  tx1cn  23105  tx2cn  23106  hauseqlcld  23142  txkgen  23148  idqtop  23202  tgqtop  23208  acufl  23413  uffix  23417  ufildr  23427  fmfg  23445  rnelfm  23449  fmfnfm  23454  fmid  23456  fmco  23457  flimrest  23479  fclsrest  23520  alexsubALT  23547  tsmsgsum  23635  tsmssubm  23639  tsmsres  23640  tsmsf1o  23641  xpsdsval  23879  blpnf  23895  blin  23919  blres  23929  xmetec  23932  imasf1obl  23989  imasf1oxms  23990  prdsbl  23992  metrest  24025  psmetutop  24068  restmetu  24071  dscopn  24074  cnbl0  24282  bl2ioo  24300  xrtgioo  24314  cncfmet  24417  icoopnst  24447  iocopnst  24448  cldcss2  24951  iunmbl2  25066  mbfmulc2lem  25156  mbfmax  25158  ismbf3d  25163  mbfimaopnlem  25164  mbfaddlem  25169  mbfsup  25173  i1f1lem  25198  i1faddlem  25202  i1fmullem  25203  i1fmulclem  25212  i1fres  25215  mbfi1fseqlem4  25228  limcdif  25385  limcnlp  25387  limcflf  25390  limcres  25395  limcun  25404  ply1remlem  25672  fta1glem2  25676  plypf1  25718  ofmulrt  25787  plyremlem  25809  aannenlem1  25833  gausslemma2dlem1a  26858  oldlim  27371  tglineelsb2  27873  tglinecom  27876  ushgredgedg  28476  ushgredgedgloop  28478  nbumgrvtx  28593  nbusgrvtxm1uvtx  28652  vdiscusgr  28778  wspniunwspnon  29167  rusgrnumwwlkb0  29215  clwwlknscsh  29305  clwwlknun  29355  eupth2lems  29481  fusgr2wsp2nb  29577  fusgreg2wsp  29579  ubthlem1  30111  ocin  30537  shscom  30560  spansncol  30809  eqsnd  31754  iunsnima  31835  iunsnima2  31836  nfpconfp  31844  unipreima  31857  2ndimaxp  31860  suppiniseg  31896  ressupprn  31900  1stpreimas  31915  1stpreima  31916  2ndpreima  31917  fpwrelmapffslem  31945  iocinioc2  31978  nndiffz1  31985  fzsplit3  31993  swrdrn3  32107  cntzun  32200  cntzsnid  32201  ecxpid  32461  qsxpid  32463  lindspropd  32488  lsmsnpridl  32497  lsmssass  32501  grplsm0l  32502  grplsmid  32503  nsgqusf1olem2  32514  nsgqusf1olem3  32515  ghmquskerlem1  32517  ghmqusker  32521  crngmxidl  32574  opprlidlabs  32588  ressply1mon1p  32646  irngnzply1  32744  smatrcl  32765  qtophaus  32805  locfinreflem  32809  rspectopn  32836  zarclsiin  32840  rhmpreimacnlem  32853  prsdm  32883  prsrn  32884  indpi1  33007  indf1ofs  33013  1stmbfm  33248  2ndmbfm  33249  mbfmcnt  33256  eulerpartlemgh  33366  dstfrvunirn  33462  reprsuc  33616  reprpmtf1o  33627  satfvsucsuc  34345  dmopab3rexdif  34385  neifg  35245  filnetlem4  35255  ontgval  35305  bj-gabima  35809  bj-restsn  35952  bj-rest10  35958  bj-restpw  35962  bj-restuni  35967  mptsnunlem  36208  finxpsuclem  36267  wl-clabtv  36448  wl-clabt  36449  poimirlem16  36493  poimirlem19  36496  poimirlem23  36500  poimirlem27  36504  heicant  36512  istotbnd3  36628  sstotbnd  36632  ismtyima  36660  heibor  36678  divrngidl  36885  eccnvep  37139  ecxrn  37246  eqvrelth  37470  disjlem19  37660  prtlem19  37737  prter2  37740  lkrsc  37956  lshpkr  37976  paddvaln0N  38661  paddval0  38670  diaglbN  39915  cdlemm10N  39978  lcfrvalsnN  40401  lcfrlem9  40410  lcdlss  40479  mapd1o  40508  mapd0  40525  hlhillcs  40822  sn-iotalem  41035  fnsnbt  41049  fsuppind  41160  mzpmfp  41471  lzunuz  41492  fz1eqin  41493  jm2.23  41721  pw2f1ocnv  41762  dfacbasgrp  41836  nnoeomeqom  42048  oadif1lem  42115  oadif1  42116  fzunt  42192  fzuntd  42193  fzunt1d  42194  fzuntgd  42195  inintabd  42316  cnvcnvintabd  42337  cnvintabd  42340  rfcnpre3  43703  rfcnpre4  43704  iindif2f  43840  rnmptpr  43859  iccshift  44218  iocopn  44220  iooshift  44222  iccintsng  44223  icoopn  44225  limcdm0  44321  limcresiooub  44345  limcresioolb  44346  fperdvper  44622  itgperiod  44684  fourierdlem32  44842  fourierdlem33  44843  fourierdlem48  44857  fourierdlem49  44858  fourierdlem81  44890  fsetsniunop  45746  elsetpreimafvrab  46049  iccpartiun  46089  mgmhmpropd  46542  rnghmval2  46679  subsubrng2  46728  subrngpropd  46732  itsclinecirc0in  47415  i0oii  47506  io1ii  47507  thincmon  47608  thincepi  47609  grptcmon  47670  grptcepi  47671