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

Theorem eqriv 2053
 Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqriv.1 (𝑥𝐴𝑥𝐵)
Assertion
Ref Expression
eqriv 𝐴 = 𝐵
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem eqriv
StepHypRef Expression
1 dfcleq 2050 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 eqriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1358 1 𝐴 = 𝐵
 Colors of variables: wff set class Syntax hints:   ↔ wb 102   = wceq 1259   ∈ 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  2784  difeqri  3091  uneqri  3112  incom  3156  ineqri  3157  difin  3201  invdif  3206  indif  3207  difundi  3216  indifdir  3220  pwv  3606  uniun  3626  intun  3673  intpr  3674  iuncom  3690  iuncom4  3691  iun0  3740  0iun  3741  iunin2  3747  iunun  3761  iunxun  3762  iunxiun  3763  iinpw  3769  inuni  3936  unidif0  3947  unipw  3980  snnex  4208  unon  4264  xpiundi  4425  xpiundir  4426  0xp  4447  iunxpf  4511  cnvuni  4548  dmiun  4571  dmuni  4572  epini  4723  rniun  4761  cnvresima  4837  imaco  4853  rnco  4854  dfmpt3  5048  imaiun  5426  opabex3d  5775  opabex3  5776  ecid  6199  qsid  6201  dfz2  8370
 Copyright terms: Public domain W3C validator