Theorem eqrdv 2728

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  eqrdav  2729  abbi  2795  eqabdv  2862  uneq1  4127  unineq  4254  difin2  4267  difsn  4765  eqsndOLD  4798  intmin4  4944  iunconst  4968  iinconst  4969  iuneqconst  4970  dfiun2g  4997  dfiun2gOLD  4998  iindif1  5042  iindif2  5044  iinin2  5045  iunxsng  5057  iunxsngf  5059  opthprc  5705  dmopab2rex  5884  dmxp  5895  epin  6069  inimasn  6132  dmsnopg  6189  dfco2a  6222  iotaeq  6479  imadif  6603  unima  6939  ssimaex  6949  unpreima  7038  respreima  7041  iinpreima  7044  fnsnbg  7141  fnsnbOLD  7143  fmptsng  7145  fmptsnd  7146  tpres  7178  iunpw  7750  ordpwsuc  7793  ordsucun  7803  fiun  7924  f1iun  7925  reldm  8026  fimaproj  8117  xpord2pred  8127  xpord3pred  8134  rntpos  8221  onoviun  8315  oarec  8529  iserd  8700  erth  8728  mapdm0  8818  mapfset  8826  ixpiin  8900  boxriin  8916  pw2f1olem  9050  fifo  9390  ordiso2  9475  ttrclse  9687  finacn  10010  acnen  10013  acacni  10101  dfac13  10103  fin23lem26  10285  isf34lem4  10337  axdc3lem2  10411  fpwwe2lem7  10597  fpwwe2lem11  10601  fpwwe2lem12  10602  gch2  10635  gchac  10641  gchina  10659  genpass  10969  1idpr  10989  eqreznegel  12900  ixxun  13329  iccid  13358  difreicc  13452  iccsplit  13453  fzsplit2  13517  fzsn  13534  fzpr  13547  uzsplit  13564  fzdif1  13573  preduz  13618  predfz  13621  fz1isolem  14433  pr2pwpr  14451  isercolllem2  15639  isercoll  15641  bitsmod  16413  bitscmp  16415  saddisj  16442  sadadd  16444  sadass  16448  smupvallem  16460  smueqlem  16467  smumul  16470  gcdcllem2  16477  vdwapun  16952  firest  17402  fncnvimaeqv  18088  mgmhmpropd  18632  mhmpropd  18726  efmnd1bas  18827  subgacs  19100  eqgid  19119  ghmmhmb  19166  ghmpropd  19195  ghmqusnsglem1  19219  ghmquskerlem1  19222  ghmqusker  19226  resscntz  19272  symg1bas  19328  lsmcom2  19592  lsmass  19606  ablnsg  19784  lsmcomx  19793  gsum2d2  19911  subgdmdprd  19973  dprd2d2  19983  2nsgsimpgd  20041  unitpropd  20333  rnghmval2  20360  subsubrng2  20480  subrngpropd  20484  subsubrg2  20515  subrgpropd  20524  rhmpropd  20525  subrgacs  20716  sdrgacs  20717  abvpropd  20751  lssacs  20880  lssats2  20913  lsspropd  20931  lmhmpropd  20987  lbspropd  21013  pzriprnglem10  21407  psdmul  22060  discld  22983  neiptopnei  23026  neiptopreu  23027  restsn  23064  restdis  23072  neitr  23074  restlp  23077  cndis  23185  cnindis  23186  cnpdis  23187  lpcls  23258  hausmapdom  23394  ptpjpre1  23465  tx1cn  23503  tx2cn  23504  hauseqlcld  23540  txkgen  23546  idqtop  23600  tgqtop  23606  acufl  23811  uffix  23815  ufildr  23825  fmfg  23843  rnelfm  23847  fmfnfm  23852  fmid  23854  fmco  23855  flimrest  23877  fclsrest  23918  alexsubALT  23945  tsmsgsum  24033  tsmssubm  24037  tsmsres  24038  tsmsf1o  24039  xpsdsval  24276  blpnf  24292  blin  24316  blres  24326  xmetec  24329  imasf1obl  24383  imasf1oxms  24384  prdsbl  24386  metrest  24419  psmetutop  24462  restmetu  24465  dscopn  24468  cnbl0  24668  bl2ioo  24687  xrtgioo  24702  cncfmet  24809  icoopnst  24843  iocopnst  24844  cldcss2  25349  iunmbl2  25465  mbfmulc2lem  25555  mbfmax  25557  ismbf3d  25562  mbfimaopnlem  25563  mbfaddlem  25568  mbfsup  25572  i1f1lem  25597  i1faddlem  25601  i1fmullem  25602  i1fmulclem  25610  i1fres  25613  mbfi1fseqlem4  25626  limcdif  25784  limcnlp  25786  limcflf  25789  limcres  25794  limcun  25803  ply1remlem  26077  fta1glem2  26081  plypf1  26124  ofmulrt  26196  plyremlem  26219  aannenlem1  26243  gausslemma2dlem1a  27283  oldlim  27805  tglineelsb2  28566  tglinecom  28569  ushgredgedg  29163  ushgredgedgloop  29165  nbumgrvtx  29280  nbusgrvtxm1uvtx  29339  vdiscusgr  29466  wspniunwspnon  29860  rusgrnumwwlkb0  29908  clwwlknscsh  29998  clwwlknun  30048  eupth2lems  30174  fusgr2wsp2nb  30270  fusgreg2wsp  30272  ubthlem1  30806  ocin  31232  shscom  31255  spansncol  31504  iunsnima  32553  iunsnima2  32554  nfpconfp  32563  unipreima  32574  2ndimaxp  32577  fdifsupp  32615  suppiniseg  32616  ressupprn  32620  1stpreimas  32636  1stpreima  32637  2ndpreima  32638  fpwrelmapffslem  32662  iocinioc2  32709  nndiffz1  32716  fzsplit3  32723  indpi1  32790  indf1ofs  32796  swrdrn3  32884  cntzun  33015  cntzsnid  33016  cntrval2  33135  ecxpid  33339  qsxpid  33340  lindspropd  33361  lsmsnpridl  33376  lsmssass  33380  grplsm0l  33381  grplsmid  33382  nsgqusf1olem2  33392  nsgqusf1olem3  33393  crngmxidl  33447  opprlidlabs  33463  rprmirredb  33510  ressply1mon1p  33544  fldextrspunlsp  33676  irngnzply1  33693  smatrcl  33793  qtophaus  33833  locfinreflem  33837  rspectopn  33864  zarclsiin  33868  rhmpreimacnlem  33881  prsdm  33911  prsrn  33912  1stmbfm  34258  2ndmbfm  34259  mbfmcnt  34266  eulerpartlemgh  34376  dstfrvunirn  34473  reprsuc  34613  reprpmtf1o  34624  satfvsucsuc  35359  dmopab3rexdif  35399  cbvabdavw  36251  neifg  36366  filnetlem4  36376  ontgval  36426  bj-gabima  36935  bj-restsn  37077  bj-rest10  37083  bj-restpw  37087  bj-restuni  37092  mptsnunlem  37333  finxpsuclem  37392  wl-clabtv  37592  wl-clabt  37593  poimirlem16  37637  poimirlem19  37640  poimirlem23  37644  poimirlem27  37648  heicant  37656  istotbnd3  37772  sstotbnd  37776  ismtyima  37804  heibor  37822  divrngidl  38029  eccnvep  38277  ecxrn  38380  eqvrelth  38609  disjlem19  38800  prtlem19  38878  prter2  38881  lkrsc  39097  lshpkr  39117  paddvaln0N  39802  paddval0  39811  diaglbN  41056  cdlemm10N  41119  lcfrvalsnN  41542  lcfrlem9  41551  lcdlss  41620  mapd1o  41649  mapd0  41666  hlhillcs  41959  grpods  42189  unitscyglem2  42191  sn-iotalem  42216  fsuppind  42585  mzpmfp  42742  lzunuz  42763  fz1eqin  42764  jm2.23  42992  pw2f1ocnv  43033  dfacbasgrp  43104  nnoeomeqom  43308  oadif1lem  43375  oadif1  43376  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  inintabd  43575  cnvcnvintabd  43596  cnvintabd  43599  rfcnpre3  45034  rfcnpre4  45035  iindif2f  45161  rnmptpr  45178  iccshift  45523  iocopn  45525  iooshift  45527  iccintsng  45528  icoopn  45530  limcdm0  45623  limcresiooub  45647  limcresioolb  45648  fperdvper  45924  itgperiod  45986  fourierdlem32  46144  fourierdlem33  46145  fourierdlem48  46159  fourierdlem49  46160  fourierdlem81  46192  fsetsniunop  47054  elsetpreimafvrab  47399  iccpartiun  47439  dfclnbgr6  47860  dfnbgr6  47861  uhgrimisgrgric  47935  clnbgrgrim  47938  stgredgiun  47961  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  itsclinecirc0in  48768  i0oii  48912  io1ii  48913  sectpropd  49030  invpropd  49032  isopropd  49034  cicpropd  49043  uobffth  49211  uobeqw  49212  natoppfb  49224  oppc1stflem  49280  thincmon  49426  thincepi  49427  termfucterm  49537  grptcmon  49586  grptcepi  49587  lanval2  49620  ranval2  49623  ranval3  49624