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

Theorem eqriv 2432
Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqriv.1  |-  ( x  e.  A  <->  x  e.  B )
Assertion
Ref Expression
eqriv  |-  A  =  B
Distinct variable groups:    x, A    x, B

Proof of Theorem eqriv
StepHypRef Expression
1 dfcleq 2429 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1559 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1652    e. wcel 1725
This theorem is referenced by:  eqid  2435  cbvab  2553  vjust  2949  nfccdeq  3151  difeqri  3459  uneqri  3481  incom  3525  ineqri  3526  indifdir  3589  undif3  3594  pwpr  4003  pwtp  4004  pwv  4006  uniun  4026  intun  4074  intpr  4075  iuncom  4091  iuncom4  4092  iun0  4139  0iun  4140  iunin2  4147  iinun2  4149  iundif2  4150  iunun  4163  iunxun  4164  iunxiun  4165  iinpw  4171  inuni  4354  unipw  4406  snnex  4705  unon  4803  xpiundi  4924  xpiundir  4925  xp0r  4948  iunxpf  5013  cnvuni  5049  dmiun  5070  dmuni  5071  epini  5226  rniun  5274  cnvresima  5351  imaco  5367  rnco  5368  dfmpt3  5559  opabex3d  5981  opabex3  5982  imaiun  5984  fparlem1  6438  fparlem2  6439  oarec  6797  ecid  6961  qsid  6962  mapval2  7035  ixpin  7079  onfin2  7290  unfilem1  7363  unifpw  7401  dfom5  7597  alephsuc2  7953  ackbij2  8115  isf33lem  8238  dffin7-2  8270  fin1a2lem6  8277  acncc  8312  fin41  8316  iunfo  8406  grutsk  8689  grothac  8697  grothtsk  8702  dfz2  10291  qexALT  10581  om2uzrani  11284  hashkf  11612  divalglem4  12908  1nprm  13076  nsgacs  14968  oppgsubm  15150  oppgsubg  15151  oppgcntz  15152  opprsubg  15733  opprunit  15758  opprirred  15799  opprsubrg  15881  00lss  16010  00ply1bas  16626  dfprm2  16766  unocv  16899  iunocv  16900  zcld  18836  iundisj  19434  plyun0  20108  aannenlem2  20238  eqid1  21753  choc0  22820  chocnul  22822  spanunsni  23073  lncnbd  23533  adjbd1o  23580  rnbra  23602  pjimai  23671  iundisjf  24021  xrdifh  24135  iundisjfi  24144  dfdm5  25392  dfrn5  25393  symdifass  25664  dffix2  25742  fixcnv  25745  dfom5b  25749  fnimage  25766  brimg  25774  prtlem16  26709  aaitgo  27335
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-cleq 2428
  Copyright terms: Public domain W3C validator