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

Theorem eqriv 2092
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 2089 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 eqriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1394 1 𝐴 = 𝐵
Colors of variables: wff set class
Syntax hints:  wb 104   = wceq 1296  wcel 1445
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1390  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-cleq 2088
This theorem is referenced by:  eqid  2095  sb8ab  2216  cbvab  2217  vjust  2634  nfccdeq  2852  difeqri  3135  uneqri  3157  incom  3207  ineqri  3208  difin  3252  invdif  3257  indif  3258  difundi  3267  indifdir  3271  pwv  3674  uniun  3694  intun  3741  intpr  3742  iuncom  3758  iuncom4  3759  iun0  3808  0iun  3809  iunin2  3815  iunun  3830  iunxun  3831  iunxiun  3832  iinpw  3841  inuni  4012  unidif0  4023  unipw  4068  snnex  4298  unon  4356  xpiundi  4525  xpiundir  4526  0xp  4547  iunxpf  4615  cnvuni  4653  dmiun  4676  dmuni  4677  epini  4836  rniun  4875  cnvresima  4954  imaco  4970  rnco  4971  dfmpt3  5170  imaiun  5577  opabex3d  5930  opabex3  5931  ecid  6395  qsid  6397  mapval2  6475  ixpin  6520  dfz2  8917  infssuzex  11372  1nprm  11523
  Copyright terms: Public domain W3C validator