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

Theorem eqrdv 2436
Description: Deduce equality of classes from equivalence of membership. (Contributed by NM, 17-Mar-1996.)
Hypothesis
Ref Expression
eqrdv.1  |-  ( ph  ->  ( x  e.  A  <->  x  e.  B ) )
Assertion
Ref Expression
eqrdv  |-  ( ph  ->  A  =  B )
Distinct variable groups:    x, A    x, B    ph, x

Proof of Theorem eqrdv
StepHypRef Expression
1 eqrdv.1 . . 3  |-  ( ph  ->  ( x  e.  A  <->  x  e.  B ) )
21alrimiv 1642 . 2  |-  ( ph  ->  A. x ( x  e.  A  <->  x  e.  B ) )
3 dfcleq 2432 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
42, 3sylibr 205 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.wal 1550    = wceq 1653    e. wcel 1726
This theorem is referenced by:  eqrdav  2437  csbcomg  3276  csbabg  3312  uneq1  3496  ineq1  3537  unineq  3593  difin2  3605  difsn  3935  intmin4  4081  iunconst  4103  iinconst  4104  dfiun2g  4125  iindif2  4162  iinin2  4163  iunxsng  4171  iunpw  4761  ordpwsuc  4797  ordsucun  4807  opthprc  4927  inimasn  5291  dmsnopg  5343  dfco2a  5372  iotaeq  5428  imadif  5530  fun11iun  5697  ssimaex  5790  unpreima  5858  respreima  5861  iinpreima  5862  fconstfv  5956  reldm  6400  rntpos  6494  onoviun  6607  oarec  6807  iserd  6933  erth  6951  map0e  7053  ixpiin  7090  boxriin  7106  pw2f1olem  7214  fifo  7439  ordiso2  7486  finacn  7933  acnen  7936  acacni  8022  dfac13  8024  fin23lem26  8207  isf34lem4  8259  axdc3lem2  8333  fpwwe2lem8  8514  fpwwe2lem12  8518  fpwwe2lem13  8519  gchac  8550  gch2  8556  gchina  8576  genpass  8888  1idpr  8908  eqreznegel  10563  ixxun  10934  iccid  10963  difreicc  11030  iccsplit  11031  fzsplit2  11078  fzsn  11096  fzpr  11103  uzsplit  11120  fz1isolem  11712  isercolllem2  12461  isercoll  12463  bitsmod  12950  bitscmp  12952  saddisj  12979  sadadd  12981  sadass  12985  smupvallem  12997  smueqlem  13004  smumul  13007  gcdcllem2  13014  vdwapun  13344  firest  13662  mhmpropd  14746  subgacs  14977  eqgid  14994  ghmmhmb  15019  ghmpropd  15045  resscntz  15132  lsmcom2  15291  lsmass  15304  ablnsg  15464  lsmcomx  15473  gsum2d2  15550  subgdmdprd  15594  dprd2d2  15604  unitpropd  15804  subsubrg2  15897  subrgpropd  15904  rhmpropd  15905  abvpropd  15932  lssacs  16045  lssats2  16078  lsspropd  16095  lmhmpropd  16147  lbspropd  16173  unitg  17034  discld  17155  neiptopnei  17198  neiptopreu  17199  restsn  17236  restdis  17244  neitr  17246  restlp  17249  cndis  17357  cnindis  17358  cnpdis  17359  lpcls  17430  hausmapdom  17565  ptpjpre1  17605  tx1cn  17643  tx2cn  17644  hauseqlcld  17680  txkgen  17686  idqtop  17740  tgqtop  17746  acufl  17951  uffix  17955  ufildr  17965  fmfg  17983  rnelfm  17987  fmfnfm  17992  fmid  17994  fmco  17995  flimrest  18017  fclsrest  18058  alexsubALT  18084  tsmsgsum  18170  tsmssubm  18174  tsmsres  18175  tsmsf1o  18176  xpsdsval  18413  blpnf  18429  blin  18453  blres  18463  xmetec  18466  imasf1obl  18520  imasf1oxms  18521  prdsbl  18523  metrest  18556  metutopOLD  18614  psmetutop  18615  restmetu  18619  dscopn  18623  cnbl0  18810  bl2ioo  18825  xrtgioo  18839  cncfmet  18940  icoopnst  18966  iocopnst  18967  cldcss2  19345  iunmbl2  19453  mbfmulc2lem  19541  mbfmax  19543  ismbf3d  19548  mbfimaopnlem  19549  mbfaddlem  19554  mbfsup  19558  i1f1lem  19583  i1faddlem  19587  i1fmullem  19588  i1fmulclem  19596  i1fres  19599  mbfi1fseqlem4  19612  limcdif  19765  limcnlp  19767  limcflf  19770  limcres  19775  limcun  19784  ply1remlem  20087  fta1glem2  20091  plypf1  20133  ofmulrt  20201  plyremlem  20223  aannenlem1  20247  cusgrarn  21470  uvtxnbgra  21504  eupath2  21704  ubthlem1  22374  ocin  22800  shscom  22823  spansncol  23072  unipreima  24058  1stpreima  24097  2ndpreima  24098  iocinioc2  24144  fzsplit3  24152  indpi1  24421  indf1ofs  24425  1stmbfm  24612  2ndmbfm  24613  mbfmcnt  24620  dstfrvunirn  24734  preduz  25477  predfz  25480  ontgval  26183  neifg  26402  filnetlem4  26412  istotbnd3  26482  sstotbnd  26486  ismtyima  26514  heibor  26532  divrngidl  26640  prtlem19  26729  prter2  26732  mzpmfp  26806  lzunuz  26828  fz1eqin  26829  jm2.23  27069  pw2f1ocnv  27110  dfacbasgrp  27252  subrgacs  27487  sdrgacs  27488  rfcnpre3  27682  rfcnpre4  27683  2wot2wont  28406  2spot2iun2spont  28411  nbhashuvtx  28420  vdiscusgra  28423  usg2spot2nb  28516  usgreg2spot  28518  lkrsc  29957  lshpkr  29977  paddvaln0N  30660  paddval0  30669  diaglbN  31915  cdlemm10N  31978  lcfrvalsnN  32401  lcfrlem9  32410  lcdlss  32479  mapd1o  32508  mapd0  32525  hlhillcs  32821
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-cleq 2431
  Copyright terms: Public domain W3C validator