Theorem eqrdv 2763

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

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

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 2156  ax-ext 2737

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

This theorem is used by:  eqrdav  2764  abbi  2830  eqabdv  2898  uneq1  4115  unineq  4241  difin2  4254  difsn  4768  intmin4  4944  intprg  4948  iunconst  4968  iinconst  4969  iuneqconst  4970  dfiun2g  4996  iindif1  5043  iindif2  5045  iinin2  5046  iunxsng  5058  iunxsngf  5060  opthprc  5727  dmopab2rex  5909  dmxp  5921  epin  6099  inimasn  6155  dmsnopg  6216  dfco2a  6249  iotaeq  6508  imadif  6624  unima  6960  ssimaex  6970  unpreima  7062  respreima  7065  iinpreima  7068  fnsnbg  7166  fnsnbOLD  7168  fmptsng  7170  fmptsnd  7171  tpres  7203  iunpw  7772  ordpwsuc  7813  ordsucun  7823  fiun  7942  f1iun  7943  reldm  8043  fimaproj  8133  xpord2pred  8143  xpord3pred  8150  rntpos  8237  onoviun  8332  oarec  8549  iserd  8723  erth  8751  mapdm0  8841  mapfset  8849  ixpiin  8924  boxriin  8940  pw2f1olem  9072  fifo  9395  ordiso2  9480  ttrclse  9699  finacn  10046  acnen  10049  acacni  10136  dfac13  10138  fin23lem26  10320  isf34lem4  10372  axdc3lem2  10446  fpwwe2lem7  10633  fpwwe2lem11  10637  fpwwe2lem12  10638  gch2  10671  gchac  10677  gchina  10695  genpass  11005  1idpr  11025  indpi1  12243  eqreznegel  12970  ixxun  13400  iccid  13429  difreicc  13523  iccsplit  13524  fzsplit2  13590  fzsn  13607  fzpr  13620  uzsplit  13637  fzdif1  13646  preduz  13691  predfz  13694  fz1isolem  14512  pr2pwpr  14530  swrdrn3  14708  isercolllem2  15737  isercoll  15739  bitsmod  16512  bitscmp  16514  saddisj  16541  sadadd  16543  sadass  16547  smupvallem  16559  smueqlem  16566  smumul  16569  gcdcllem2  16576  vdwapun  17052  firest  17503  fncnvimaeqv  18194  mgmhmpropd  18778  mhmpropd  18874  efmnd1bas  18976  subgacs  19251  ecxpid  19266  qsxpid  19267  eqgid  19272  ghmmhmb  19321  ghmpropd  19350  ghmqusnsglem1  19374  ghmquskerlem1  19377  ghmqusker  19381  resscntz  19427  symg1bas  19485  lsmcom2  19749  lsmass  19763  ablnsg  19941  lsmcomx  19950  gsum2d2  20068  subgdmdprd  20130  dprd2d2  20140  2nsgsimpgd  20198  unitpropd  20525  rnghmval2  20552  subsubrng2  20693  subrngpropd  20697  subsubrg2  20728  subrgpropd  20737  rhmpropd  20738  subrgacs  20933  sdrgacs  20934  abvpropd  20968  lssacs  21118  lssats2  21151  lsspropd  21168  lmhmpropd  21224  lbspropd  21250  pzriprnglem10  21670  psdmul  22359  discld  23276  neiptopnei  23319  neiptopreu  23320  restsn  23357  restdis  23365  neitr  23367  restlp  23370  cndis  23478  cnindis  23479  cnpdis  23480  lpcls  23551  hausmapdom  23688  ptpjpre1  23759  tx1cn  23797  tx2cn  23798  hauseqlcld  23834  txkgen  23840  idqtop  23894  tgqtop  23900  acufl  24105  uffix  24109  ufildr  24119  fmfg  24137  rnelfm  24141  fmfnfm  24146  fmid  24148  fmco  24149  flimrest  24171  fclsrest  24212  alexsubALT  24239  tsmsgsum  24327  tsmssubm  24331  tsmsres  24332  tsmsf1o  24333  xpsdsval  24569  blpnf  24585  blin  24609  blres  24619  xmetec  24622  imasf1obl  24676  imasf1oxms  24677  prdsbl  24679  metrest  24712  psmetutop  24755  restmetu  24758  dscopn  24761  cnbl0  24961  bl2ioo  24980  xrtgioo  24995  cncfmet  25099  icoopnst  25129  iocopnst  25130  cldcss2  25632  iunmbl2  25747  mbfmulc2lem  25837  mbfmax  25839  ismbf3d  25844  mbfimaopnlem  25845  mbfaddlem  25850  mbfsup  25854  i1f1lem  25879  i1faddlem  25883  i1fmullem  25884  i1fmulclem  25892  i1fres  25895  mbfi1fseqlem4  25908  limcdif  26066  limcnlp  26068  limcflf  26071  limcres  26076  limcun  26085  ply1remlem  26353  fta1glem2  26357  plypf1  26400  ofmulrt  26471  plyremlem  26496  aannenlem1  26522  gausslemma2dlem1a  27560  oldlim  28111  negleft  28282  negright  28283  tglineelsb2  28936  tglinecom  28939  ushgredgedg  29613  ushgredgedgloop  29615  nbumgrvtx  29730  nbusgrvtxm1uvtx  29789  vdiscusgr  29915  wspniunwspnon  30315  rusgrnumwwlkb0  30366  clwwlknscsh  30456  clwwlknun  30506  eupth2lems  30636  fusgr2wsp2nb  30732  fusgreg2wsp  30734  ubthlem1  31269  ocin  31695  shscom  31718  spansncol  31967  iunsnima  33010  iunsnima2  33011  nfpconfp  33024  unipreima  33035  2ndimaxp  33038  fdifsupp  33077  suppiniseg  33078  ressupprn  33082  1stpreimas  33098  1stpreima  33099  2ndpreima  33100  fpwrelmapffslem  33123  iocinioc2  33170  nndiffz1  33177  fzsplit3  33184  indf1ofs  33232  cntzun  33439  cntzsnid  33440  cntrval2  33531  lindspropd  33736  lsmsnpridl  33749  lsmssass  33751  grplsm0l  33752  grplsmid  33753  nsgqusf1olem2  33763  nsgqusf1olem3  33764  crngmxidl  33792  opprlidlabs  33807  rprmirredb  33862  ressply1mon1p  33898  fldextrspunlsp  34104  irngnzply1  34121  smatrcl  34226  qtophaus  34266  locfinreflem  34270  rspectopn  34297  zarclsiin  34301  rhmpreimacnlem  34314  prsdm  34344  prsrn  34345  1stmbfm  34691  2ndmbfm  34692  mbfmcnt  34699  eulerpartlemgh  34809  dstfrvunirn  34906  reprsuc  35043  reprpmtf1o  35054  satfvsucsuc  35870  dmopab3rexdif  35910  cbvabdavw  36801  neifg  36915  filnetlem4  36925  ontgval  36975  bj-gabima  37609  bj-restsn  37757  bj-rest10  37763  bj-restpw  37767  bj-restuni  37772  mptsnunlem  38017  finxpsuclem  38076  wl-clabtv  38274  wl-clabt  38275  poimirlem16  38320  poimirlem19  38323  poimirlem23  38327  poimirlem27  38331  heicant  38339  istotbnd3  38455  sstotbnd  38459  ismtyima  38487  heibor  38505  divrngidl  38712  eccnvep  38970  ecxrn  39088  eqvrelth  39377  disjlem19  39586  prtlem19  39685  prter2  39688  lkrsc  39904  lshpkr  39924  paddvaln0N  40608  paddval0  40617  diaglbN  41862  cdlemm10N  41925  lcfrvalsnN  42348  lcfrlem9  42357  lcdlss  42426  mapd1o  42455  mapd0  42472  hlhillcs  42765  grpods  42994  unitscyglem2  42996  sn-iotalem  43025  fsuppind  43355  mzpmfp  43511  lzunuz  43532  fz1eqin  43533  jm2.23  43756  pw2f1ocnv  43797  dfacbasgrp  43868  nnoeomeqom  44072  oadif1lem  44139  oadif1  44140  fzunt  44214  fzuntd  44215  fzunt1d  44216  fzuntgd  44217  inintabd  44338  cnvcnvintabd  44359  cnvintabd  44362  rfcnpre3  45786  rfcnpre4  45787  iindif2f  45911  rnmptpr  45928  iccshift  46267  iocopn  46269  iooshift  46271  iccintsng  46272  icoopn  46274  limcdm0  46367  limcresiooub  46389  limcresioolb  46390  fperdvper  46666  itgperiod  46728  fourierdlem32  46886  fourierdlem33  46887  fourierdlem48  46901  fourierdlem49  46902  fourierdlem81  46934  fsetsniunop  47819  elsetpreimafvrab  48176  iccpartiun  48216  dfclnbgr6  48654  dfnbgr6  48655  uhgrimisgrgric  48729  clnbgrgrim  48732  stgredgiun  48756  gpgnbgrvtx0  48872  gpgnbgrvtx1  48873  itsclinecirc0in  49588  i0oii  49731  io1ii  49732  sectpropd  49848  invpropd  49850  isopropd  49852  cicpropd  49861  uobffth  50029  uobeqw  50030  natoppfb  50042  oppc1stflem  50098  thincmon  50244  thincepi  50245  termfucterm  50355  grptcmon  50404  grptcepi  50405  lanval2  50438  ranval2  50441  ranval3  50442