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

Theorem eqriv 2114
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 2111 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1414 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 104    = wceq 1316    e. wcel 1465
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 1410  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  eqid  2117  sb8ab  2239  cbvab  2240  vjust  2661  nfccdeq  2880  difeqri  3166  uneqri  3188  incom  3238  ineqri  3239  difin  3283  invdif  3288  indif  3289  difundi  3298  indifdir  3302  pwv  3705  uniun  3725  intun  3772  intpr  3773  iuncom  3789  iuncom4  3790  iun0  3839  0iun  3840  iunin2  3846  iunun  3861  iunxun  3862  iunxiun  3864  iinpw  3873  inuni  4050  unidif0  4061  unipw  4109  snnex  4339  unon  4397  xpiundi  4567  xpiundir  4568  0xp  4589  iunxpf  4657  cnvuni  4695  dmiun  4718  dmuni  4719  epini  4880  rniun  4919  cnvresima  4998  imaco  5014  rnco  5015  dfmpt3  5215  imaiun  5629  opabex3d  5987  opabex3  5988  ecid  6460  qsid  6462  mapval2  6540  ixpin  6585  dfz2  9081  infssuzex  11554  1nprm  11707
  Copyright terms: Public domain W3C validator