Theorem eqrdv 2735

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 2730	. 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 2709

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

This theorem is referenced by:  eqrdav  2736  abbi  2802  eqabdv  2870  uneq1  4102  unineq  4229  difin2  4242  difsn  4742  eqsndOLD  4775  intmin4  4920  intprg  4924  iunconst  4944  iinconst  4945  iuneqconst  4946  dfiun2g  4973  iindif1  5018  iindif2  5020  iinin2  5021  iunxsng  5033  iunxsngf  5035  opthprc  5688  dmopab2rex  5866  dmxp  5878  epin  6054  inimasn  6114  dmsnopg  6171  dfco2a  6204  iotaeq  6460  imadif  6576  unima  6909  ssimaex  6919  unpreima  7009  respreima  7012  iinpreima  7015  fnsnbg  7112  fnsnbOLD  7114  fmptsng  7116  fmptsnd  7117  tpres  7149  iunpw  7718  ordpwsuc  7759  ordsucun  7769  fiun  7889  f1iun  7890  reldm  7990  fimaproj  8078  xpord2pred  8088  xpord3pred  8095  rntpos  8182  onoviun  8276  oarec  8490  iserd  8663  erth  8691  mapdm0  8782  mapfset  8790  ixpiin  8865  boxriin  8881  pw2f1olem  9012  fifo  9338  ordiso2  9423  ttrclse  9639  finacn  9963  acnen  9966  acacni  10054  dfac13  10056  fin23lem26  10238  isf34lem4  10290  axdc3lem2  10364  fpwwe2lem7  10551  fpwwe2lem11  10555  fpwwe2lem12  10556  gch2  10589  gchac  10595  gchina  10613  genpass  10923  1idpr  10943  indpi1  12164  eqreznegel  12875  ixxun  13305  iccid  13334  difreicc  13428  iccsplit  13429  fzsplit2  13494  fzsn  13511  fzpr  13524  uzsplit  13541  fzdif1  13550  preduz  13595  predfz  13598  fz1isolem  14414  pr2pwpr  14432  isercolllem2  15619  isercoll  15621  bitsmod  16396  bitscmp  16398  saddisj  16425  sadadd  16427  sadass  16431  smupvallem  16443  smueqlem  16450  smumul  16453  gcdcllem2  16460  vdwapun  16936  firest  17386  fncnvimaeqv  18077  mgmhmpropd  18657  mhmpropd  18751  efmnd1bas  18852  subgacs  19127  eqgid  19146  ghmmhmb  19193  ghmpropd  19222  ghmqusnsglem1  19246  ghmquskerlem1  19249  ghmqusker  19253  resscntz  19299  symg1bas  19357  lsmcom2  19621  lsmass  19635  ablnsg  19813  lsmcomx  19822  gsum2d2  19940  subgdmdprd  20002  dprd2d2  20012  2nsgsimpgd  20070  unitpropd  20388  rnghmval2  20415  subsubrng2  20532  subrngpropd  20536  subsubrg2  20567  subrgpropd  20576  rhmpropd  20577  subrgacs  20768  sdrgacs  20769  abvpropd  20803  lssacs  20953  lssats2  20986  lsspropd  21004  lmhmpropd  21060  lbspropd  21086  pzriprnglem10  21480  psdmul  22142  discld  23064  neiptopnei  23107  neiptopreu  23108  restsn  23145  restdis  23153  neitr  23155  restlp  23158  cndis  23266  cnindis  23267  cnpdis  23268  lpcls  23339  hausmapdom  23475  ptpjpre1  23546  tx1cn  23584  tx2cn  23585  hauseqlcld  23621  txkgen  23627  idqtop  23681  tgqtop  23687  acufl  23892  uffix  23896  ufildr  23906  fmfg  23924  rnelfm  23928  fmfnfm  23933  fmid  23935  fmco  23936  flimrest  23958  fclsrest  23999  alexsubALT  24026  tsmsgsum  24114  tsmssubm  24118  tsmsres  24119  tsmsf1o  24120  xpsdsval  24356  blpnf  24372  blin  24396  blres  24406  xmetec  24409  imasf1obl  24463  imasf1oxms  24464  prdsbl  24466  metrest  24499  psmetutop  24542  restmetu  24545  dscopn  24548  cnbl0  24748  bl2ioo  24767  xrtgioo  24782  cncfmet  24886  icoopnst  24916  iocopnst  24917  cldcss2  25419  iunmbl2  25534  mbfmulc2lem  25624  mbfmax  25626  ismbf3d  25631  mbfimaopnlem  25632  mbfaddlem  25637  mbfsup  25641  i1f1lem  25666  i1faddlem  25670  i1fmullem  25671  i1fmulclem  25679  i1fres  25682  mbfi1fseqlem4  25695  limcdif  25853  limcnlp  25855  limcflf  25858  limcres  25863  limcun  25872  ply1remlem  26140  fta1glem2  26144  plypf1  26187  ofmulrt  26258  plyremlem  26281  aannenlem1  26305  gausslemma2dlem1a  27342  oldlim  27893  negleft  28064  negright  28065  tglineelsb2  28714  tglinecom  28717  ushgredgedg  29312  ushgredgedgloop  29314  nbumgrvtx  29429  nbusgrvtxm1uvtx  29488  vdiscusgr  29615  wspniunwspnon  30006  rusgrnumwwlkb0  30057  clwwlknscsh  30147  clwwlknun  30197  eupth2lems  30323  fusgr2wsp2nb  30419  fusgreg2wsp  30421  ubthlem1  30956  ocin  31382  shscom  31405  spansncol  31654  iunsnima  32706  iunsnima2  32707  nfpconfp  32720  unipreima  32731  2ndimaxp  32734  fdifsupp  32773  suppiniseg  32774  ressupprn  32778  1stpreimas  32794  1stpreima  32795  2ndpreima  32796  fpwrelmapffslem  32820  iocinioc2  32867  nndiffz1  32874  fzsplit3  32881  indf1ofs  32941  swrdrn3  33030  cntzun  33155  cntzsnid  33156  cntrval2  33247  ecxpid  33436  qsxpid  33437  lindspropd  33458  lsmsnpridl  33473  lsmssass  33477  grplsm0l  33478  grplsmid  33479  nsgqusf1olem2  33489  nsgqusf1olem3  33490  crngmxidl  33544  opprlidlabs  33560  rprmirredb  33607  ressply1mon1p  33643  fldextrspunlsp  33834  irngnzply1  33851  smatrcl  33956  qtophaus  33996  locfinreflem  34000  rspectopn  34027  zarclsiin  34031  rhmpreimacnlem  34044  prsdm  34074  prsrn  34075  1stmbfm  34420  2ndmbfm  34421  mbfmcnt  34428  eulerpartlemgh  34538  dstfrvunirn  34635  reprsuc  34775  reprpmtf1o  34786  satfvsucsuc  35563  dmopab3rexdif  35603  cbvabdavw  36454  neifg  36569  filnetlem4  36579  ontgval  36629  bj-gabima  37263  bj-restsn  37410  bj-rest10  37416  bj-restpw  37420  bj-restuni  37425  mptsnunlem  37668  finxpsuclem  37727  wl-clabtv  37925  wl-clabt  37926  poimirlem16  37971  poimirlem19  37974  poimirlem23  37978  poimirlem27  37982  heicant  37990  istotbnd3  38106  sstotbnd  38110  ismtyima  38138  heibor  38156  divrngidl  38363  eccnvep  38623  ecxrn  38741  eqvrelth  39030  disjlem19  39239  prtlem19  39338  prter2  39341  lkrsc  39557  lshpkr  39577  paddvaln0N  40261  paddval0  40270  diaglbN  41515  cdlemm10N  41578  lcfrvalsnN  42001  lcfrlem9  42010  lcdlss  42079  mapd1o  42108  mapd0  42125  hlhillcs  42418  grpods  42647  unitscyglem2  42649  sn-iotalem  42676  fsuppind  43037  mzpmfp  43193  lzunuz  43214  fz1eqin  43215  jm2.23  43442  pw2f1ocnv  43483  dfacbasgrp  43554  nnoeomeqom  43758  oadif1lem  43825  oadif1  43826  fzunt  43900  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  inintabd  44024  cnvcnvintabd  44045  cnvintabd  44048  rfcnpre3  45482  rfcnpre4  45483  iindif2f  45608  rnmptpr  45625  iccshift  45966  iocopn  45968  iooshift  45970  iccintsng  45971  icoopn  45973  limcdm0  46066  limcresiooub  46088  limcresioolb  46089  fperdvper  46365  itgperiod  46427  fourierdlem32  46585  fourierdlem33  46586  fourierdlem48  46600  fourierdlem49  46601  fourierdlem81  46633  fsetsniunop  47509  elsetpreimafvrab  47866  iccpartiun  47906  dfclnbgr6  48344  dfnbgr6  48345  uhgrimisgrgric  48419  clnbgrgrim  48422  stgredgiun  48446  gpgnbgrvtx0  48562  gpgnbgrvtx1  48563  itsclinecirc0in  49263  i0oii  49407  io1ii  49408  sectpropd  49524  invpropd  49526  isopropd  49528  cicpropd  49537  uobffth  49705  uobeqw  49706  natoppfb  49718  oppc1stflem  49774  thincmon  49920  thincepi  49921  termfucterm  50031  grptcmon  50080  grptcepi  50081  lanval2  50114  ranval2  50117  ranval3  50118