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

Theorem eqriv 2186
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 2183 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 eqriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1464 1 𝐴 = 𝐵
Colors of variables: wff set class
Syntax hints:  wb 105   = wceq 1364  wcel 2160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182
This theorem is referenced by:  eqid  2189  sb8ab  2311  cbvabw  2312  cbvab  2313  vjust  2753  nfccdeq  2975  csbcow  3083  difeqri  3270  uneqri  3292  incom  3342  ineqri  3343  difin  3387  invdif  3392  indif  3393  difundi  3402  indifdir  3406  pwv  3823  uniun  3843  intun  3890  intpr  3891  iuncom  3907  iuncom4  3908  iun0  3958  0iun  3959  iunin2  3965  iunun  3980  iunxun  3981  iunxiun  3983  iinpw  3992  inuni  4173  unidif0  4185  unipw  4235  snnex  4466  unon  4528  xpiundi  4702  xpiundir  4703  0xp  4724  iunxpf  4793  cnvuni  4831  dmiun  4854  dmuni  4855  epini  5017  rniun  5057  cnvresima  5136  imaco  5152  rnco  5153  dfmpt3  5357  imaiun  5782  opabex3d  6146  opabex3  6147  ecid  6624  qsid  6626  mapval2  6704  ixpin  6749  dfz2  9355  dfrp2  10294  infssuzex  11982  1nprm  12146  infpn2  12507
  Copyright terms: Public domain W3C validator