MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqrdv Structured version   Visualization version   GIF version

Theorem eqrdv 2608
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
StepHypRef Expression
1 eqrdv.1 . . 3 (𝜑 → (𝑥𝐴𝑥𝐵))
21alrimiv 1842 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝑥𝐵))
3 dfcleq 2604 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
42, 3sylibr 223 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wal 1473   = wceq 1475  wcel 1977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-cleq 2603
This theorem is referenced by:  eqrdav  2609  uneq1  3722  ineq1  3769  unineq  3836  difin2  3849  difsn  4269  intmin4  4436  iunconst  4460  iinconst  4461  dfiun2g  4483  iindif2  4520  iinin2  4521  iunxsng  4533  opthprc  5079  inimasn  5455  dmsnopg  5510  dfco2a  5538  iotaeq  5762  imadif  5873  ssimaex  6158  unpreima  6234  respreima  6237  iinpreima  6238  fnsnb  6315  fmptsng  6317  fmptsnd  6318  tpres  6349  iunpw  6848  ordpwsuc  6885  ordsucun  6895  fun11iun  6997  reldm  7088  rntpos  7230  onoviun  7305  oarec  7507  iserd  7633  erth  7656  map0e  7759  ixpiin  7798  boxriin  7814  pw2f1olem  7927  fifo  8199  ordiso2  8281  finacn  8734  acnen  8737  acacni  8823  dfac13  8825  fin23lem26  9008  isf34lem4  9060  axdc3lem2  9134  fpwwe2lem8  9316  fpwwe2lem12  9320  fpwwe2lem13  9321  gch2  9354  gchac  9360  gchina  9378  genpass  9688  1idpr  9708  eqreznegel  11609  ixxun  12021  iccid  12050  difreicc  12134  iccsplit  12135  fzsplit2  12195  fzsn  12212  fzpr  12224  uzsplit  12239  preduz  12288  predfz  12291  fz1isolem  13057  pr2pwpr  13069  isercolllem2  14193  isercoll  14195  bitsmod  14945  bitscmp  14947  saddisj  14974  sadadd  14976  sadass  14980  smupvallem  14992  smueqlem  14999  smumul  15002  gcdcllem2  15009  vdwapun  15465  firest  15865  fncnvimaeqv  16532  mhmpropd  17113  subgacs  17401  eqgid  17418  ghmmhmb  17443  ghmpropd  17470  resscntz  17536  symg1bas  17588  lsmcom2  17842  lsmass  17855  ablnsg  18022  lsmcomx  18031  gsum2d2  18145  subgdmdprd  18205  dprd2d2  18215  unitpropd  18469  subsubrg2  18579  subrgpropd  18586  rhmpropd  18587  abvpropd  18614  lssacs  18737  lssats2  18770  lsspropd  18787  lmhmpropd  18843  lbspropd  18869  discld  20651  neiptopnei  20694  neiptopreu  20695  restsn  20732  restdis  20740  neitr  20742  restlp  20745  cndis  20853  cnindis  20854  cnpdis  20855  lpcls  20926  hausmapdom  21061  ptpjpre1  21132  tx1cn  21170  tx2cn  21171  hauseqlcld  21207  txkgen  21213  idqtop  21267  tgqtop  21273  acufl  21479  uffix  21483  ufildr  21493  fmfg  21511  rnelfm  21515  fmfnfm  21520  fmid  21522  fmco  21523  flimrest  21545  fclsrest  21586  alexsubALT  21613  tsmsgsum  21700  tsmssubm  21704  tsmsres  21705  tsmsf1o  21706  xpsdsval  21944  blpnf  21960  blin  21984  blres  21994  xmetec  21997  imasf1obl  22051  imasf1oxms  22052  prdsbl  22054  metrest  22087  psmetutop  22130  restmetu  22133  dscopn  22136  cnbl0  22335  bl2ioo  22351  xrtgioo  22365  cncfmet  22467  icoopnst  22494  iocopnst  22495  cldcss2  22966  iunmbl2  23077  mbfmulc2lem  23165  mbfmax  23167  ismbf3d  23172  mbfimaopnlem  23173  mbfaddlem  23178  mbfsup  23182  i1f1lem  23207  i1faddlem  23211  i1fmullem  23212  i1fmulclem  23220  i1fres  23223  mbfi1fseqlem4  23236  limcdif  23391  limcnlp  23393  limcflf  23396  limcres  23401  limcun  23410  ply1remlem  23671  fta1glem2  23675  plypf1  23717  ofmulrt  23786  plyremlem  23808  aannenlem1  23832  gausslemma2dlem1a  24835  tglineelsb2  25273  tglinecom  25276  cusgrarn  25782  uvtxnbgra  25815  clwwlknscsh  26141  2wot2wont  26207  2spot2iun2spont  26212  nbhashuvtx  26237  vdiscusgra  26242  rusgranumwlkb0  26274  eupath2  26301  usg2spot2nb  26386  usgreg2spot  26388  numclwwlkun  26400  ubthlem1  26904  ocin  27333  shscom  27356  spansncol  27605  iunxsngf  28552  iunsnima  28602  unipreima  28620  1stpreimas  28660  1stpreima  28661  2ndpreima  28662  fpwrelmapffslem  28689  iocinioc2  28725  nndiffz1  28730  fzsplit3  28734  smatrcl  28984  fimaproj  29022  qtophaus  29025  locfinreflem  29029  prsdm  29082  prsrn  29083  indpi1  29205  indf1ofs  29209  1stmbfm  29443  2ndmbfm  29444  mbfmcnt  29451  eulerpartlemgh  29561  dstfrvunirn  29657  neifg  31330  filnetlem4  31340  ontgval  31394  bj-restsn  32010  bj-rest10  32016  bj-restpw  32020  bj-restuni  32025  mptsnunlem  32155  finxpsuclem  32204  poimirlem16  32389  poimirlem19  32392  poimirlem23  32396  poimirlem27  32400  heicant  32408  istotbnd3  32534  sstotbnd  32538  ismtyima  32566  heibor  32584  divrngidl  32791  prtlem19  32975  prter2  32978  lkrsc  33196  lshpkr  33216  paddvaln0N  33899  paddval0  33908  diaglbN  35156  cdlemm10N  35219  lcfrvalsnN  35642  lcfrlem9  35651  lcdlss  35720  mapd1o  35749  mapd0  35766  hlhillcs  36062  mzpmfp  36122  lzunuz  36143  fz1eqin  36144  jm2.23  36375  pw2f1ocnv  36416  dfacbasgrp  36491  subrgacs  36583  sdrgacs  36584  inintabd  36698  cnvcnvintabd  36719  cnvintabd  36722  csbabgOLD  37866  rfcnpre3  38009  rfcnpre4  38010  iunxsngf2  38049  unima  38134  iccshift  38385  iocopn  38387  iooshift  38389  iccintsng  38390  icoopn  38392  limcdm0  38479  limcresiooub  38503  limcresioolb  38504  fperdvper  38602  itgperiod  38667  fourierdlem32  38826  fourierdlem33  38827  fourierdlem48  38841  fourierdlem49  38842  fourierdlem81  38874  iccpartiun  39767  ushgredgedga  40448  ushgredgedgaloop  40450  nbumgrvtx  40560  nbusgrvtxm1uvtx  40624  vdiscusgr  40739  wspniunwspnon  41122  rusgrnumwwlkb0  41166  clwwlksnscsh  41239  clwwlksnun  41273  eupth2lems  41398  fusgr2wsp2nb  41490  fusgreg2wsp  41492  mgmhmpropd  41567  rnghmval2  41677
  Copyright terms: Public domain W3C validator