ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqriv Unicode version

Theorem eqriv 2112
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 2109 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1412 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 104    = wceq 1314    e. wcel 1463
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1408  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  eqid  2115  sb8ab  2237  cbvab  2238  vjust  2659  nfccdeq  2878  difeqri  3164  uneqri  3186  incom  3236  ineqri  3237  difin  3281  invdif  3286  indif  3287  difundi  3296  indifdir  3300  pwv  3703  uniun  3723  intun  3770  intpr  3771  iuncom  3787  iuncom4  3788  iun0  3837  0iun  3838  iunin2  3844  iunun  3859  iunxun  3860  iunxiun  3862  iinpw  3871  inuni  4048  unidif0  4059  unipw  4107  snnex  4337  unon  4395  xpiundi  4565  xpiundir  4566  0xp  4587  iunxpf  4655  cnvuni  4693  dmiun  4716  dmuni  4717  epini  4878  rniun  4917  cnvresima  4996  imaco  5012  rnco  5013  dfmpt3  5213  imaiun  5627  opabex3d  5985  opabex3  5986  ecid  6458  qsid  6460  mapval2  6538  ixpin  6583  dfz2  9074  infssuzex  11538  1nprm  11691
  Copyright terms: Public domain W3C validator