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

Theorem eqriv 2053
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 2050 . 2  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
2 eqriv.1 . 2  |-  ( x  e.  A  <->  x  e.  B )
31, 2mpgbir 1358 1  |-  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 102    = wceq 1259    e. wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  eqid  2056  sb8ab  2175  cbvab  2176  vjust  2575  nfccdeq  2785  difeqri  3092  uneqri  3113  incom  3157  ineqri  3158  difin  3202  invdif  3207  indif  3208  difundi  3217  indifdir  3221  pwv  3607  uniun  3627  intun  3674  intpr  3675  iuncom  3691  iuncom4  3692  iun0  3741  0iun  3742  iunin2  3748  iunun  3762  iunxun  3763  iunxiun  3764  iinpw  3770  inuni  3937  unidif0  3948  unipw  3981  snnex  4209  unon  4265  xpiundi  4426  xpiundir  4427  0xp  4448  iunxpf  4512  cnvuni  4549  dmiun  4572  dmuni  4573  epini  4724  rniun  4762  cnvresima  4838  imaco  4854  rnco  4855  dfmpt3  5049  imaiun  5427  opabex3d  5776  opabex3  5777  ecid  6200  qsid  6202  dfz2  8371
  Copyright terms: Public domain W3C validator