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

Theorem eqriv 2037
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 2034 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 eqriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1342 1 𝐴 = 𝐵
Colors of variables: wff set class
Syntax hints:  wb 98   = wceq 1243  wcel 1393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  eqid  2040  sb8ab  2159  cbvab  2160  vjust  2558  nfccdeq  2762  difeqri  3064  uneqri  3085  incom  3129  ineqri  3130  difin  3174  invdif  3179  indif  3180  difundi  3189  indifdir  3193  pwv  3579  uniun  3599  intun  3646  intpr  3647  iuncom  3663  iuncom4  3664  iun0  3713  0iun  3714  iunin2  3720  iunun  3734  iunxun  3735  iunxiun  3736  iinpw  3742  inuni  3909  unidif0  3920  unipw  3953  snnex  4181  unon  4237  xpiundi  4398  xpiundir  4399  0xp  4420  iunxpf  4484  cnvuni  4521  dmiun  4544  dmuni  4545  epini  4696  rniun  4734  cnvresima  4810  imaco  4826  rnco  4827  dfmpt3  5021  imaiun  5399  opabex3d  5748  opabex3  5749  ecid  6169  qsid  6171  dfz2  8311
  Copyright terms: Public domain W3C validator