Theorem eqrdv 2758

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  eqrdav  2759  abbi  2825  eqabdv  2893  uneq1  4159  unineq  4232  difin2  4245  difsn  4757  intmin4  4936  intprg  4940  iunconst  4960  iinconst  4961  iuneqconst  4962  dfiun2g  4987  iindif1  5034  iindif2  5036  iinin2  5037  iunxsng  5049  iunxsngf  5051  opthprc  5714  dmopab2rex  5899  dmxp  5911  epin  6094  inimasn  6147  dmsnopg  6216  dfco2a  6249  iotaeq  6508  imadif  6627  unima  6963  ssimaex  6973  unpreima  7065  respreima  7068  iinpreima  7072  fnsnbg  7172  fmptsng  7175  fmptsnd  7176  tpres  7209  iunpw  7787  ordpwsuc  7828  ordsucun  7838  fiun  7957  f1iun  7958  reldm  8057  fimaproj  8156  xpord2pred  8166  xpord3pred  8173  rntpos  8261  onoviun  8356  oarec  8575  iserd  8749  erth  8777  mapdm0  8867  mapfset  8877  ixpiin  8957  boxriin  8973  pw2f1olem  9105  fifo  9429  ordiso2  9514  ttrclse  9733  finacn  10134  acnen  10137  acacni  10224  dfac13  10226  fin23lem26  10408  isf34lem4  10460  axdc3lem2  10534  fpwwe2lem7  10727  fpwwe2lem11  10731  fpwwe2lem12  10732  gch2  10765  gchac  10771  gchina  10789  genpass  11099  1idpr  11119  indpi1  12339  eqreznegel  13066  ixxun  13497  iccid  13526  difreicc  13620  iccsplit  13621  fzsplit2  13688  fzsn  13705  fzpr  13718  uzsplit  13735  fzdif1  13744  preduz  13789  predfz  13792  fz1isolem  14611  pr2pwpr  14629  swrdrn3  14808  isercolllem2  15840  isercoll  15842  bitsmod  16613  bitscmp  16615  saddisj  16642  sadadd  16644  sadass  16648  smupvallem  16660  smueqlem  16667  smumul  16670  gcdcllem2  16677  vdwapun  17159  firest  17610  fncnvimaeqv  18301  mgmhmpropd  18894  mhmpropd  18994  efmnd1bas  19096  subgacs  19378  ecxpid  19393  qsxpid  19394  eqgid  19399  ghmmhmb  19448  ghmpropd  19477  ghmqusnsglem1  19501  ghmquskerlem1  19504  ghmqusker  19508  resscntz  19554  symg1bas  19612  lsmcom2  19876  lsmass  19890  ablnsg  20068  lsmcomx  20077  gsum2d2  20195  subgdmdprd  20257  dprd2d2  20267  2nsgsimpgd  20325  unitpropd  20654  rnghmval2  20681  subsubrng2  20823  subrngpropd  20827  subsubrg2  20858  subrgpropd  20867  rhmpropd  20868  subrgacs  21064  sdrgacs  21065  abvpropd  21099  lssacs  21249  lssats2  21282  lsspropd  21299  lmhmpropd  21355  lbspropd  21381  pzriprnglem10  21803  psdmul  22494  discld  23414  neiptopnei  23457  neiptopreu  23458  restsn  23495  restdis  23503  neitr  23505  restlp  23508  cndis  23616  cnindis  23617  cnpdis  23618  lpcls  23689  hausmapdom  23826  ptpjpre1  23897  tx1cn  23935  tx2cn  23936  hauseqlcld  23972  txkgen  23978  idqtop  24032  tgqtop  24038  acufl  24243  uffix  24247  ufildr  24257  fmfg  24275  rnelfm  24279  fmfnfm  24284  fmid  24286  fmco  24287  flimrest  24309  fclsrest  24350  alexsubALT  24377  tsmsgsum  24465  tsmssubm  24469  tsmsres  24470  tsmsf1o  24471  xpsdsval  24707  blpnf  24723  blin  24747  blres  24757  xmetec  24760  imasf1obl  24814  imasf1oxms  24815  prdsbl  24817  metrest  24850  psmetutop  24893  restmetu  24896  dscopn  24899  cnbl0  25099  bl2ioo  25118  xrtgioo  25133  cncfmet  25237  icoopnst  25267  iocopnst  25268  cldcss2  25770  iunmbl2  25885  mbfmulc2lem  25975  mbfmax  25977  ismbf3d  25982  mbfimaopnlem  25983  mbfaddlem  25988  mbfsup  25992  i1f1lem  26017  i1faddlem  26021  i1fmullem  26022  i1fmulclem  26030  i1fres  26033  mbfi1fseqlem4  26046  limcdif  26203  limcnlp  26205  limcflf  26208  limcres  26213  limcun  26222  ply1remlem  26490  fta1glem2  26494  plypf1  26538  ofmulrt  26607  plyremlem  26632  rnplynfin  26637  aannenlem1  26662  gausslemma2dlem1a  27699  oldlim  28280  negleft  28451  negright  28452  tglineelsb2  29107  tglinecom  29110  angmgmaddcpbl  29397  ushgredgedg  29817  ushgredgedgloop  29819  nbumgrvtx  29934  nbusgrvtxm1uvtx  29993  vdiscusgr  30119  wspniunwspnon  30519  rusgrnumwwlkb0  30570  clwwlknscsh  30660  clwwlknun  30710  eupth2lems  30846  fusgr2wsp2nb  30942  fusgreg2wsp  30944  ubthlem1  31479  ocin  31905  shscom  31928  spansncol  32177  iunsnima  33261  iunsnima2  33262  nfpconfp  33275  unipreima  33286  2ndimaxp  33289  fdifsupp  33327  suppiniseg  33328  ressupprn  33332  1stpreimas  33348  1stpreima  33349  2ndpreima  33350  fpwrelmapffslem  33372  iocinioc2  33419  nndiffz1  33426  fzsplit3  33433  indf1ofs  33481  cntzun  33688  cntzsnid  33689  cntrval2  33780  lindspropd  33986  lsmsnpridl  33999  lsmssass  34001  grplsm0l  34002  grplsmid  34003  nsgqusf1olem2  34013  nsgqusf1olem3  34014  crngmxidl  34042  opprlidlabs  34057  rprmirredb  34112  ressply1mon1p  34148  fldextrspunlsp  34354  irngnzply1  34371  smatrcl  34476  qtophaus  34516  locfinreflem  34520  rspectopn  34547  zarclsiin  34551  rhmpreimacnlem  34564  prsdm  34594  prsrn  34595  1stmbfm  34940  2ndmbfm  34941  mbfmcnt  34948  eulerpartlemgh  35058  dstfrvunirn  35155  reprsuc  35292  reprpmtf1o  35303  satfvsucsuc  36218  dmopab3rexdif  36258  cbvabdavw  37139  neifg  37253  filnetlem4  37263  ontgval  37313  bj-gabima  37947  bj-restsn  38109  bj-rest10  38115  bj-restpw  38119  bj-restuni  38124  mptsnunlem  38368  finxpsuclem  38427  wl-clabtv  38625  wl-clabt  38626  poimirlem16  38661  poimirlem19  38664  poimirlem23  38668  poimirlem27  38672  heicant  38680  istotbnd3  38812  sstotbnd  38816  ismtyima  38844  heibor  38862  divrngidl  39069  eccnvep  39327  ecxrn  39445  eqvrelth  39734  disjlem19  39943  prtlem19  40042  prter2  40045  lkrsc  40261  lshpkr  40281  paddvaln0N  40965  paddval0  40974  diaglbN  42219  cdlemm10N  42282  lcfrvalsnN  42705  lcfrlem9  42714  lcdlss  42783  mapd1o  42812  mapd0  42829  hlhillcs  43122  grpods  43351  unitscyglem2  43353  sn-iotalem  43382  fsuppind  43725  mzpmfp  43865  lzunuz  43886  fz1eqin  43887  jm2.23  44110  pw2f1ocnv  44151  dfacbasgrp  44217  nnoeomeqom  44421  oadif1lem  44488  oadif1  44489  fzunt  44563  fzuntd  44564  fzunt1d  44565  fzuntgd  44566  inintabd  44687  cnvcnvintabd  44707  cnvintabd  44710  rfcnpre3  46157  rfcnpre4  46158  iindif2f  46282  rnmptpr  46299  iccshift  46637  iocopn  46639  iooshift  46641  iccintsng  46642  icoopn  46644  limcdm0  46737  limcresiooub  46759  limcresioolb  46760  fperdvper  47036  itgperiod  47098  fourierdlem32  47256  fourierdlem33  47257  fourierdlem48  47271  fourierdlem49  47272  fourierdlem81  47304  fsetsniunop  48226  elsetpreimafvrab  48583  iccpartiun  48623  dfclnbgr6  49061  dfnbgr6  49062  uhgrimisgrgric  49136  clnbgrgrim  49139  stgredgiun  49163  gpgnbgrvtx0  49279  gpgnbgrvtx1  49280  itsclinecirc0in  49994  i0oii  50141  io1ii  50142  sectpropd  50258  invpropd  50260  isopropd  50262  cicpropd  50271  uobffth  50441  uobeqw  50442  natoppfb  50460  oppc1stflem  50516  thincmon  50675  thincepi  50676  termfucterm  50789  grptcmon  50838  grptcepi  50839  lanval2  50917  ranval2  50920  ranval3  50921