Theorem eqrdv 2724

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1532   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718

This theorem is referenced by:  eqrdav  2725  abbi  2794  eqabdv  2860  uneq1  4153  unineq  4276  difin2  4290  difsn  4797  eqsndOLD  4830  intmin4  4977  iunconst  5002  iinconst  5003  iuneqconst  5004  dfiun2g  5030  dfiun2gOLD  5031  iindif1  5075  iindif2  5077  iinin2  5078  iunxsng  5090  iunxsngf  5092  opthprc  5738  dmopab2rex  5916  epin  6097  inimasn  6159  dmsnopg  6216  dfco2a  6249  iotaeq  6511  imadif  6635  unima  6969  ssimaex  6979  unpreima  7068  respreima  7071  iinpreima  7074  fnsnb  7172  fmptsng  7174  fmptsnd  7175  tpres  7210  iunpw  7771  ordpwsuc  7816  ordsucun  7826  fiun  7948  f1iun  7949  reldm  8050  fimaproj  8141  xpord2pred  8151  xpord3pred  8158  rntpos  8246  onoviun  8365  oarec  8584  iserd  8752  erth  8777  mapdm0  8863  mapfset  8871  ixpiin  8945  boxriin  8961  pw2f1olem  9106  fifo  9468  ordiso2  9551  ttrclse  9763  finacn  10086  acnen  10089  acacni  10176  dfac13  10178  fin23lem26  10359  isf34lem4  10411  axdc3lem2  10485  fpwwe2lem7  10671  fpwwe2lem11  10675  fpwwe2lem12  10676  gch2  10709  gchac  10715  gchina  10733  genpass  11043  1idpr  11063  eqreznegel  12964  ixxun  13388  iccid  13417  difreicc  13509  iccsplit  13510  fzsplit2  13574  fzsn  13591  fzpr  13604  uzsplit  13621  preduz  13671  predfz  13674  fz1isolem  14475  pr2pwpr  14493  isercolllem2  15665  isercoll  15667  bitsmod  16431  bitscmp  16433  saddisj  16460  sadadd  16462  sadass  16466  smupvallem  16478  smueqlem  16485  smumul  16488  gcdcllem2  16495  vdwapun  16971  firest  17442  fncnvimaeqv  18138  mgmhmpropd  18686  mhmpropd  18777  efmnd1bas  18878  subgacs  19151  eqgid  19170  ghmmhmb  19217  ghmpropd  19246  ghmqusnsglem1  19270  ghmquskerlem1  19273  ghmqusker  19277  resscntz  19323  symg1bas  19384  lsmcom2  19649  lsmass  19663  ablnsg  19841  lsmcomx  19850  gsum2d2  19968  subgdmdprd  20030  dprd2d2  20040  2nsgsimpgd  20098  unitpropd  20395  rnghmval2  20422  subsubrng2  20542  subrngpropd  20546  subsubrg2  20579  subrgpropd  20588  rhmpropd  20589  subrgacs  20775  sdrgacs  20776  abvpropd  20810  lssacs  20940  lssats2  20973  lsspropd  20991  lmhmpropd  21047  lbspropd  21073  pzriprnglem10  21476  psdmul  22156  discld  23081  neiptopnei  23124  neiptopreu  23125  restsn  23162  restdis  23170  neitr  23172  restlp  23175  cndis  23283  cnindis  23284  cnpdis  23285  lpcls  23356  hausmapdom  23492  ptpjpre1  23563  tx1cn  23601  tx2cn  23602  hauseqlcld  23638  txkgen  23644  idqtop  23698  tgqtop  23704  acufl  23909  uffix  23913  ufildr  23923  fmfg  23941  rnelfm  23945  fmfnfm  23950  fmid  23952  fmco  23953  flimrest  23975  fclsrest  24016  alexsubALT  24043  tsmsgsum  24131  tsmssubm  24135  tsmsres  24136  tsmsf1o  24137  xpsdsval  24375  blpnf  24391  blin  24415  blres  24425  xmetec  24428  imasf1obl  24485  imasf1oxms  24486  prdsbl  24488  metrest  24521  psmetutop  24564  restmetu  24567  dscopn  24570  cnbl0  24778  bl2ioo  24796  xrtgioo  24810  cncfmet  24917  icoopnst  24951  iocopnst  24952  cldcss2  25458  iunmbl2  25574  mbfmulc2lem  25664  mbfmax  25666  ismbf3d  25671  mbfimaopnlem  25672  mbfaddlem  25677  mbfsup  25681  i1f1lem  25706  i1faddlem  25710  i1fmullem  25711  i1fmulclem  25720  i1fres  25723  mbfi1fseqlem4  25736  limcdif  25893  limcnlp  25895  limcflf  25898  limcres  25903  limcun  25912  ply1remlem  26189  fta1glem2  26193  plypf1  26236  ofmulrt  26306  plyremlem  26329  aannenlem1  26353  gausslemma2dlem1a  27391  oldlim  27907  tglineelsb2  28556  tglinecom  28559  ushgredgedg  29162  ushgredgedgloop  29164  nbumgrvtx  29279  nbusgrvtxm1uvtx  29338  vdiscusgr  29465  wspniunwspnon  29854  rusgrnumwwlkb0  29902  clwwlknscsh  29992  clwwlknun  30042  eupth2lems  30168  fusgr2wsp2nb  30264  fusgreg2wsp  30266  ubthlem1  30800  ocin  31226  shscom  31249  spansncol  31498  iunsnima  32538  iunsnima2  32539  nfpconfp  32549  unipreima  32561  2ndimaxp  32564  suppiniseg  32598  ressupprn  32602  1stpreimas  32617  1stpreima  32618  2ndpreima  32619  fpwrelmapffslem  32646  iocinioc2  32684  nndiffz1  32691  fzsplit3  32699  swrdrn3  32822  cntzun  32933  cntzsnid  32934  ecxpid  33242  qsxpid  33243  lindspropd  33264  lsmsnpridl  33279  lsmssass  33283  grplsm0l  33284  grplsmid  33285  nsgqusf1olem2  33295  nsgqusf1olem3  33296  crngmxidl  33350  opprlidlabs  33366  rprmirredb  33413  ressply1mon1p  33446  irngnzply1  33573  smatrcl  33624  qtophaus  33664  locfinreflem  33668  rspectopn  33695  zarclsiin  33699  rhmpreimacnlem  33712  prsdm  33742  prsrn  33743  indpi1  33866  indf1ofs  33872  1stmbfm  34107  2ndmbfm  34108  mbfmcnt  34115  eulerpartlemgh  34225  dstfrvunirn  34321  reprsuc  34474  reprpmtf1o  34485  satfvsucsuc  35206  dmopab3rexdif  35246  neifg  36096  filnetlem4  36106  ontgval  36156  bj-gabima  36659  bj-restsn  36802  bj-rest10  36808  bj-restpw  36812  bj-restuni  36817  mptsnunlem  37058  finxpsuclem  37117  wl-clabtv  37305  wl-clabt  37306  poimirlem16  37350  poimirlem19  37353  poimirlem23  37357  poimirlem27  37361  heicant  37369  istotbnd3  37485  sstotbnd  37489  ismtyima  37517  heibor  37535  divrngidl  37742  eccnvep  37993  ecxrn  38098  eqvrelth  38322  disjlem19  38512  prtlem19  38589  prter2  38592  lkrsc  38808  lshpkr  38828  paddvaln0N  39513  paddval0  39522  diaglbN  40767  cdlemm10N  40830  lcfrvalsnN  41253  lcfrlem9  41262  lcdlss  41331  mapd1o  41360  mapd0  41377  hlhillcs  41674  grpods  41906  unitscyglem2  41908  sn-iotalem  41965  fnsnbt  41976  fsuppind  42280  mzpmfp  42441  lzunuz  42462  fz1eqin  42463  jm2.23  42691  pw2f1ocnv  42732  dfacbasgrp  42806  nnoeomeqom  43015  oadif1lem  43082  oadif1  43083  fzunt  43159  fzuntd  43160  fzunt1d  43161  fzuntgd  43162  inintabd  43283  cnvcnvintabd  43304  cnvintabd  43307  rfcnpre3  44669  rfcnpre4  44670  iindif2f  44801  rnmptpr  44820  iccshift  45172  iocopn  45174  iooshift  45176  iccintsng  45177  icoopn  45179  limcdm0  45275  limcresiooub  45299  limcresioolb  45300  fperdvper  45576  itgperiod  45638  fourierdlem32  45796  fourierdlem33  45797  fourierdlem48  45811  fourierdlem49  45812  fourierdlem81  45844  fsetsniunop  46700  elsetpreimafvrab  47002  iccpartiun  47042  dfclnbgr6  47459  dfnbgr6  47460  uhgrimisgrgric  47514  clnbgrgrim  47517  itsclinecirc0in  48199  i0oii  48289  io1ii  48290  thincmon  48391  thincepi  48392  grptcmon  48453  grptcepi  48454