Theorem eqrdv 2817

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1529   = wceq 1531   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812

This theorem is referenced by:  eqrdav  2818  abbi1  2882  abbi2dv  2948  uneq1  4130  ineq1OLD  4180  unineq  4252  difin2  4264  difsn  4723  intmin4  4896  iunconst  4919  iinconst  4920  iuneqconst  4921  dfiun2g  4946  dfiun2gOLD  4947  iindif1  4988  iindif2  4990  iinin2  4991  iunxsng  5003  iunxsngf  5005  opthprc  5609  dmopab2rex  5779  inimasn  6006  dmsnopg  6063  dfco2a  6092  iotaeq  6319  imadif  6431  unima  6732  ssimaex  6741  unpreima  6826  respreima  6829  iinpreima  6830  fnsnb  6921  fmptsng  6923  fmptsnd  6924  tpres  6956  iunpw  7485  ordpwsuc  7522  ordsucun  7532  fiun  7636  f1iun  7637  reldm  7735  fimaproj  7821  rntpos  7897  onoviun  7972  oarec  8180  iserd  8307  erth  8330  mapdm0  8413  ixpiin  8480  boxriin  8496  pw2f1olem  8613  fifo  8888  ordiso2  8971  finacn  9468  acnen  9471  acacni  9558  dfac13  9560  fin23lem26  9739  isf34lem4  9791  axdc3lem2  9865  fpwwe2lem8  10051  fpwwe2lem12  10055  fpwwe2lem13  10056  gch2  10089  gchac  10095  gchina  10113  genpass  10423  1idpr  10443  eqreznegel  12326  ixxun  12746  iccid  12775  difreicc  12862  iccsplit  12863  fzsplit2  12924  fzsn  12941  fzpr  12954  uzsplit  12971  preduz  13021  predfz  13024  fz1isolem  13811  pr2pwpr  13829  isercolllem2  15014  isercoll  15016  bitsmod  15777  bitscmp  15779  saddisj  15806  sadadd  15808  sadass  15812  smupvallem  15824  smueqlem  15831  smumul  15834  gcdcllem2  15841  vdwapun  16302  firest  16698  fncnvimaeqv  17362  mhmpropd  17954  efmnd1bas  18050  subgacs  18305  eqgid  18324  ghmmhmb  18361  ghmpropd  18388  resscntz  18454  symg1bas  18511  lsmcom2  18772  lsmass  18787  ablnsg  18959  lsmcomx  18968  gsum2d2  19086  subgdmdprd  19148  dprd2d2  19158  2nsgsimpgd  19216  unitpropd  19439  subsubrg2  19554  subrgpropd  19562  rhmpropd  19563  subrgacs  19571  sdrgacs  19572  abvpropd  19605  lssacs  19731  lssats2  19764  lsspropd  19781  lmhmpropd  19837  lbspropd  19863  discld  21689  neiptopnei  21732  neiptopreu  21733  restsn  21770  restdis  21778  neitr  21780  restlp  21783  cndis  21891  cnindis  21892  cnpdis  21893  lpcls  21964  hausmapdom  22100  ptpjpre1  22171  tx1cn  22209  tx2cn  22210  hauseqlcld  22246  txkgen  22252  idqtop  22306  tgqtop  22312  acufl  22517  uffix  22521  ufildr  22531  fmfg  22549  rnelfm  22553  fmfnfm  22558  fmid  22560  fmco  22561  flimrest  22583  fclsrest  22624  alexsubALT  22651  tsmsgsum  22739  tsmssubm  22743  tsmsres  22744  tsmsf1o  22745  xpsdsval  22983  blpnf  22999  blin  23023  blres  23033  xmetec  23036  imasf1obl  23090  imasf1oxms  23091  prdsbl  23093  metrest  23126  psmetutop  23169  restmetu  23172  dscopn  23175  cnbl0  23374  bl2ioo  23392  xrtgioo  23406  cncfmet  23508  icoopnst  23535  iocopnst  23536  cldcss2  24037  iunmbl2  24150  mbfmulc2lem  24240  mbfmax  24242  ismbf3d  24247  mbfimaopnlem  24248  mbfaddlem  24253  mbfsup  24257  i1f1lem  24282  i1faddlem  24286  i1fmullem  24287  i1fmulclem  24295  i1fres  24298  mbfi1fseqlem4  24311  limcdif  24466  limcnlp  24468  limcflf  24471  limcres  24476  limcun  24485  ply1remlem  24748  fta1glem2  24752  plypf1  24794  ofmulrt  24863  plyremlem  24885  aannenlem1  24909  gausslemma2dlem1a  25933  tglineelsb2  26410  tglinecom  26413  ushgredgedg  27003  ushgredgedgloop  27005  nbumgrvtx  27120  nbusgrvtxm1uvtx  27179  vdiscusgr  27305  wspniunwspnon  27694  rusgrnumwwlkb0  27742  clwwlknscsh  27833  clwwlknun  27883  eupth2lems  28009  fusgr2wsp2nb  28105  fusgreg2wsp  28107  ubthlem1  28639  ocin  29065  shscom  29088  spansncol  29337  eqsnd  30281  iunsnima  30361  nfpconfp  30369  unipreima  30383  1stpreimas  30433  1stpreima  30434  2ndpreima  30435  fpwrelmapffslem  30460  iocinioc2  30494  nndiffz1  30501  fzsplit3  30509  swrdrn3  30622  cntzun  30688  cntzsnid  30689  ecxpid  30918  qsxpid  30920  lindspropd  30936  lsmsnpridl  30941  smatrcl  31054  qtophaus  31093  locfinreflem  31097  prsdm  31150  prsrn  31151  indpi1  31272  indf1ofs  31278  1stmbfm  31511  2ndmbfm  31512  mbfmcnt  31519  eulerpartlemgh  31629  dstfrvunirn  31725  reprsuc  31879  reprpmtf1o  31890  satfvsucsuc  32605  dmopab3rexdif  32645  neifg  33712  filnetlem4  33722  ontgval  33772  bj-restsn  34365  bj-rest10  34371  bj-restpw  34375  bj-restuni  34380  mptsnunlem  34611  finxpsuclem  34670  wl-clabtv  34821  wl-clabt  34822  wl-dfrabf  34856  poimirlem16  34900  poimirlem19  34903  poimirlem23  34907  poimirlem27  34911  heicant  34919  istotbnd3  35041  sstotbnd  35045  ismtyima  35073  heibor  35091  divrngidl  35298  eccnvep  35531  ecxrn  35631  eqvrelth  35838  prtlem19  36006  prter2  36009  lkrsc  36225  lshpkr  36245  paddvaln0N  36929  paddval0  36938  diaglbN  38183  cdlemm10N  38246  lcfrvalsnN  38669  lcfrlem9  38678  lcdlss  38747  mapd1o  38776  mapd0  38793  hlhillcs  39086  fnsnbt  39111  mzpmfp  39335  lzunuz  39356  fz1eqin  39357  jm2.23  39584  pw2f1ocnv  39625  dfacbasgrp  39699  inintabd  39930  cnvcnvintabd  39951  cnvintabd  39954  rfcnpre3  41281  rfcnpre4  41282  rnmptpr  41423  iccshift  41784  iocopn  41786  iooshift  41788  iccintsng  41789  icoopn  41791  limcdm0  41889  limcresiooub  41913  limcresioolb  41914  fperdvper  42193  itgperiod  42256  fourierdlem32  42415  fourierdlem33  42416  fourierdlem48  42430  fourierdlem49  42431  fourierdlem81  42463  elsetpreimafvrab  43545  iccpartiun  43585  mgmhmpropd  44043  rnghmval2  44157  itsclinecirc0in  44753