Theorem eqrdv 2759

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753

This theorem is used by:  eqrdav  2760  abbi  2826  eqabdv  2894  uneq1  4108  unineq  4234  difin2  4247  difsn  4761  intmin4  4937  intprg  4941  iunconst  4961  iinconst  4962  iuneqconst  4963  dfiun2g  4988  iindif1  5035  iindif2  5037  iinin2  5038  iunxsng  5050  iunxsngf  5052  opthprc  5715  dmopab2rex  5899  dmxp  5911  epin  6093  inimasn  6146  dmsnopg  6213  dfco2a  6246  iotaeq  6505  imadif  6622  unima  6958  ssimaex  6968  unpreima  7060  respreima  7063  iinpreima  7067  fnsnbg  7167  fnsnbOLD  7169  fmptsng  7171  fmptsnd  7172  tpres  7205  iunpw  7783  ordpwsuc  7824  ordsucun  7834  fiun  7953  f1iun  7954  reldm  8053  fimaproj  8145  xpord2pred  8155  xpord3pred  8162  rntpos  8249  onoviun  8344  oarec  8563  iserd  8737  erth  8765  mapdm0  8855  mapfset  8865  ixpiin  8945  boxriin  8961  pw2f1olem  9093  fifo  9417  ordiso2  9502  ttrclse  9721  finacn  10122  acnen  10125  acacni  10212  dfac13  10214  fin23lem26  10396  isf34lem4  10448  axdc3lem2  10522  fpwwe2lem7  10715  fpwwe2lem11  10719  fpwwe2lem12  10720  gch2  10753  gchac  10759  gchina  10777  genpass  11087  1idpr  11107  indpi1  12327  eqreznegel  13054  ixxun  13485  iccid  13514  difreicc  13608  iccsplit  13609  fzsplit2  13676  fzsn  13693  fzpr  13706  uzsplit  13723  fzdif1  13732  preduz  13777  predfz  13780  fz1isolem  14599  pr2pwpr  14617  swrdrn3  14795  isercolllem2  15826  isercoll  15828  bitsmod  16599  bitscmp  16601  saddisj  16628  sadadd  16630  sadass  16634  smupvallem  16646  smueqlem  16653  smumul  16656  gcdcllem2  16663  vdwapun  17145  firest  17596  fncnvimaeqv  18287  mgmhmpropd  18880  mhmpropd  18980  efmnd1bas  19082  subgacs  19364  ecxpid  19379  qsxpid  19380  eqgid  19385  ghmmhmb  19434  ghmpropd  19463  ghmqusnsglem1  19487  ghmquskerlem1  19490  ghmqusker  19494  resscntz  19540  symg1bas  19598  lsmcom2  19862  lsmass  19876  ablnsg  20054  lsmcomx  20063  gsum2d2  20181  subgdmdprd  20243  dprd2d2  20253  2nsgsimpgd  20311  unitpropd  20640  rnghmval2  20667  subsubrng2  20809  subrngpropd  20813  subsubrg2  20844  subrgpropd  20853  rhmpropd  20854  subrgacs  21050  sdrgacs  21051  abvpropd  21085  lssacs  21235  lssats2  21268  lsspropd  21285  lmhmpropd  21341  lbspropd  21367  pzriprnglem10  21789  psdmul  22480  discld  23400  neiptopnei  23443  neiptopreu  23444  restsn  23481  restdis  23489  neitr  23491  restlp  23494  cndis  23602  cnindis  23603  cnpdis  23604  lpcls  23675  hausmapdom  23812  ptpjpre1  23883  tx1cn  23921  tx2cn  23922  hauseqlcld  23958  txkgen  23964  idqtop  24018  tgqtop  24024  acufl  24229  uffix  24233  ufildr  24243  fmfg  24261  rnelfm  24265  fmfnfm  24270  fmid  24272  fmco  24273  flimrest  24295  fclsrest  24336  alexsubALT  24363  tsmsgsum  24451  tsmssubm  24455  tsmsres  24456  tsmsf1o  24457  xpsdsval  24693  blpnf  24709  blin  24733  blres  24743  xmetec  24746  imasf1obl  24800  imasf1oxms  24801  prdsbl  24803  metrest  24836  psmetutop  24879  restmetu  24882  dscopn  24885  cnbl0  25085  bl2ioo  25104  xrtgioo  25119  cncfmet  25223  icoopnst  25253  iocopnst  25254  cldcss2  25756  iunmbl2  25871  mbfmulc2lem  25961  mbfmax  25963  ismbf3d  25968  mbfimaopnlem  25969  mbfaddlem  25974  mbfsup  25978  i1f1lem  26003  i1faddlem  26007  i1fmullem  26008  i1fmulclem  26016  i1fres  26019  mbfi1fseqlem4  26032  limcdif  26189  limcnlp  26191  limcflf  26194  limcres  26199  limcun  26208  ply1remlem  26476  fta1glem2  26480  plypf1  26524  ofmulrt  26593  plyremlem  26618  rnplynfin  26623  aannenlem1  26648  gausslemma2dlem1a  27685  oldlim  28266  negleft  28437  negright  28438  tglineelsb2  29093  tglinecom  29096  angmgmaddcpbl  29383  ushgredgedg  29803  ushgredgedgloop  29805  nbumgrvtx  29920  nbusgrvtxm1uvtx  29979  vdiscusgr  30105  wspniunwspnon  30505  rusgrnumwwlkb0  30556  clwwlknscsh  30646  clwwlknun  30696  eupth2lems  30832  fusgr2wsp2nb  30928  fusgreg2wsp  30930  ubthlem1  31465  ocin  31891  shscom  31914  spansncol  32163  iunsnima  33205  iunsnima2  33206  nfpconfp  33219  unipreima  33230  2ndimaxp  33233  fdifsupp  33271  suppiniseg  33272  ressupprn  33276  1stpreimas  33292  1stpreima  33293  2ndpreima  33294  fpwrelmapffslem  33317  iocinioc2  33364  nndiffz1  33371  fzsplit3  33378  indf1ofs  33426  cntzun  33633  cntzsnid  33634  cntrval2  33725  lindspropd  33931  lsmsnpridl  33944  lsmssass  33946  grplsm0l  33947  grplsmid  33948  nsgqusf1olem2  33958  nsgqusf1olem3  33959  crngmxidl  33987  opprlidlabs  34002  rprmirredb  34057  ressply1mon1p  34093  fldextrspunlsp  34299  irngnzply1  34316  smatrcl  34421  qtophaus  34461  locfinreflem  34465  rspectopn  34492  zarclsiin  34496  rhmpreimacnlem  34509  prsdm  34539  prsrn  34540  1stmbfm  34885  2ndmbfm  34886  mbfmcnt  34893  eulerpartlemgh  35003  dstfrvunirn  35100  reprsuc  35237  reprpmtf1o  35248  satfvsucsuc  36109  dmopab3rexdif  36149  cbvabdavw  37025  neifg  37139  filnetlem4  37149  ontgval  37199  bj-gabima  37833  bj-restsn  37983  bj-rest10  37989  bj-restpw  37993  bj-restuni  37998  mptsnunlem  38241  finxpsuclem  38300  wl-clabtv  38498  wl-clabt  38499  poimirlem16  38534  poimirlem19  38537  poimirlem23  38541  poimirlem27  38545  heicant  38553  istotbnd3  38685  sstotbnd  38689  ismtyima  38717  heibor  38735  divrngidl  38942  eccnvep  39200  ecxrn  39318  eqvrelth  39607  disjlem19  39816  prtlem19  39915  prter2  39918  lkrsc  40134  lshpkr  40154  paddvaln0N  40838  paddval0  40847  diaglbN  42092  cdlemm10N  42155  lcfrvalsnN  42578  lcfrlem9  42587  lcdlss  42656  mapd1o  42685  mapd0  42702  hlhillcs  42995  grpods  43224  unitscyglem2  43226  sn-iotalem  43255  fsuppind  43598  mzpmfp  43737  lzunuz  43758  fz1eqin  43759  jm2.23  43982  pw2f1ocnv  44023  dfacbasgrp  44094  nnoeomeqom  44298  oadif1lem  44365  oadif1  44366  fzunt  44440  fzuntd  44441  fzunt1d  44442  fzuntgd  44443  inintabd  44564  cnvcnvintabd  44585  cnvintabd  44588  rfcnpre3  46019  rfcnpre4  46020  iindif2f  46144  rnmptpr  46161  iccshift  46499  iocopn  46501  iooshift  46503  iccintsng  46504  icoopn  46506  limcdm0  46599  limcresiooub  46621  limcresioolb  46622  fperdvper  46898  itgperiod  46960  fourierdlem32  47118  fourierdlem33  47119  fourierdlem48  47133  fourierdlem49  47134  fourierdlem81  47166  fsetsniunop  48088  elsetpreimafvrab  48445  iccpartiun  48485  dfclnbgr6  48923  dfnbgr6  48924  uhgrimisgrgric  48998  clnbgrgrim  49001  stgredgiun  49025  gpgnbgrvtx0  49141  gpgnbgrvtx1  49142  itsclinecirc0in  49856  i0oii  49997  io1ii  49998  sectpropd  50114  invpropd  50116  isopropd  50118  cicpropd  50127  uobffth  50295  uobeqw  50296  natoppfb  50308  oppc1stflem  50364  thincmon  50510  thincepi  50511  termfucterm  50621  grptcmon  50670  grptcepi  50671  lanval2  50704  ranval2  50707  ranval3  50708