Theorem eqrdv 2821

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816

This theorem is referenced by:  eqrdav  2822  abbi1  2886  abbi2dv  2952  uneq1  4134  ineq1OLD  4184  unineq  4256  difin2  4268  difsn  4733  intmin4  4907  iunconst  4930  iinconst  4931  iuneqconst  4932  dfiun2g  4957  dfiun2gOLD  4958  iindif1  4999  iindif2  5001  iinin2  5002  iunxsng  5014  iunxsngf  5016  opthprc  5618  dmopab2rex  5788  inimasn  6015  dmsnopg  6072  dfco2a  6101  iotaeq  6328  imadif  6440  unima  6741  ssimaex  6750  unpreima  6835  respreima  6838  iinpreima  6839  fnsnb  6930  fmptsng  6932  fmptsnd  6933  tpres  6965  iunpw  7495  ordpwsuc  7532  ordsucun  7542  fiun  7646  f1iun  7647  reldm  7745  fimaproj  7831  rntpos  7907  onoviun  7982  oarec  8190  iserd  8317  erth  8340  mapdm0  8423  ixpiin  8490  boxriin  8506  pw2f1olem  8623  fifo  8898  ordiso2  8981  finacn  9478  acnen  9481  acacni  9568  dfac13  9570  fin23lem26  9749  isf34lem4  9801  axdc3lem2  9875  fpwwe2lem8  10061  fpwwe2lem12  10065  fpwwe2lem13  10066  gch2  10099  gchac  10105  gchina  10123  genpass  10433  1idpr  10453  eqreznegel  12337  ixxun  12757  iccid  12786  difreicc  12873  iccsplit  12874  fzsplit2  12935  fzsn  12952  fzpr  12965  uzsplit  12982  preduz  13032  predfz  13035  fz1isolem  13822  pr2pwpr  13840  isercolllem2  15024  isercoll  15026  bitsmod  15787  bitscmp  15789  saddisj  15816  sadadd  15818  sadass  15822  smupvallem  15834  smueqlem  15841  smumul  15844  gcdcllem2  15851  vdwapun  16312  firest  16708  fncnvimaeqv  17372  mhmpropd  17964  efmnd1bas  18060  subgacs  18315  eqgid  18334  ghmmhmb  18371  ghmpropd  18398  resscntz  18464  symg1bas  18521  lsmcom2  18782  lsmass  18797  ablnsg  18969  lsmcomx  18978  gsum2d2  19096  subgdmdprd  19158  dprd2d2  19168  2nsgsimpgd  19226  unitpropd  19449  subsubrg2  19564  subrgpropd  19572  rhmpropd  19573  subrgacs  19581  sdrgacs  19582  abvpropd  19615  lssacs  19741  lssats2  19774  lsspropd  19791  lmhmpropd  19847  lbspropd  19873  discld  21699  neiptopnei  21742  neiptopreu  21743  restsn  21780  restdis  21788  neitr  21790  restlp  21793  cndis  21901  cnindis  21902  cnpdis  21903  lpcls  21974  hausmapdom  22110  ptpjpre1  22181  tx1cn  22219  tx2cn  22220  hauseqlcld  22256  txkgen  22262  idqtop  22316  tgqtop  22322  acufl  22527  uffix  22531  ufildr  22541  fmfg  22559  rnelfm  22563  fmfnfm  22568  fmid  22570  fmco  22571  flimrest  22593  fclsrest  22634  alexsubALT  22661  tsmsgsum  22749  tsmssubm  22753  tsmsres  22754  tsmsf1o  22755  xpsdsval  22993  blpnf  23009  blin  23033  blres  23043  xmetec  23046  imasf1obl  23100  imasf1oxms  23101  prdsbl  23103  metrest  23136  psmetutop  23179  restmetu  23182  dscopn  23185  cnbl0  23384  bl2ioo  23402  xrtgioo  23416  cncfmet  23518  icoopnst  23545  iocopnst  23546  cldcss2  24047  iunmbl2  24160  mbfmulc2lem  24250  mbfmax  24252  ismbf3d  24257  mbfimaopnlem  24258  mbfaddlem  24263  mbfsup  24267  i1f1lem  24292  i1faddlem  24296  i1fmullem  24297  i1fmulclem  24305  i1fres  24308  mbfi1fseqlem4  24321  limcdif  24476  limcnlp  24478  limcflf  24481  limcres  24486  limcun  24495  ply1remlem  24758  fta1glem2  24762  plypf1  24804  ofmulrt  24873  plyremlem  24895  aannenlem1  24919  gausslemma2dlem1a  25943  tglineelsb2  26420  tglinecom  26423  ushgredgedg  27013  ushgredgedgloop  27015  nbumgrvtx  27130  nbusgrvtxm1uvtx  27189  vdiscusgr  27315  wspniunwspnon  27704  rusgrnumwwlkb0  27752  clwwlknscsh  27843  clwwlknun  27893  eupth2lems  28019  fusgr2wsp2nb  28115  fusgreg2wsp  28117  ubthlem1  28649  ocin  29075  shscom  29098  spansncol  29347  eqsnd  30291  iunsnima  30371  nfpconfp  30379  unipreima  30393  1stpreimas  30443  1stpreima  30444  2ndpreima  30445  fpwrelmapffslem  30470  iocinioc2  30504  nndiffz1  30511  fzsplit3  30519  swrdrn3  30631  cntzun  30697  cntzsnid  30698  ecxpid  30927  qsxpid  30929  lindspropd  30945  lsmsnpridl  30950  smatrcl  31063  qtophaus  31102  locfinreflem  31106  prsdm  31159  prsrn  31160  indpi1  31281  indf1ofs  31287  1stmbfm  31520  2ndmbfm  31521  mbfmcnt  31528  eulerpartlemgh  31638  dstfrvunirn  31734  reprsuc  31888  reprpmtf1o  31899  satfvsucsuc  32614  dmopab3rexdif  32654  neifg  33721  filnetlem4  33731  ontgval  33781  bj-restsn  34375  bj-rest10  34381  bj-restpw  34385  bj-restuni  34390  mptsnunlem  34621  finxpsuclem  34680  wl-clabtv  34831  wl-clabt  34832  wl-dfrabf  34866  poimirlem16  34910  poimirlem19  34913  poimirlem23  34917  poimirlem27  34921  heicant  34929  istotbnd3  35051  sstotbnd  35055  ismtyima  35083  heibor  35101  divrngidl  35308  eccnvep  35541  ecxrn  35641  eqvrelth  35848  prtlem19  36016  prter2  36019  lkrsc  36235  lshpkr  36255  paddvaln0N  36939  paddval0  36948  diaglbN  38193  cdlemm10N  38256  lcfrvalsnN  38679  lcfrlem9  38688  lcdlss  38757  mapd1o  38786  mapd0  38803  hlhillcs  39096  fnsnbt  39127  mzpmfp  39351  lzunuz  39372  fz1eqin  39373  jm2.23  39600  pw2f1ocnv  39641  dfacbasgrp  39715  inintabd  39946  cnvcnvintabd  39967  cnvintabd  39970  rfcnpre3  41297  rfcnpre4  41298  rnmptpr  41440  iccshift  41801  iocopn  41803  iooshift  41805  iccintsng  41806  icoopn  41808  limcdm0  41906  limcresiooub  41930  limcresioolb  41931  fperdvper  42210  itgperiod  42273  fourierdlem32  42431  fourierdlem33  42432  fourierdlem48  42446  fourierdlem49  42447  fourierdlem81  42479  elsetpreimafvrab  43561  iccpartiun  43601  mgmhmpropd  44059  rnghmval2  44173  itsclinecirc0in  44769