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

Theorem eqriv 2085
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 2082 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 eqriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1387 1 𝐴 = 𝐵
Colors of variables: wff set class
Syntax hints:  wb 103   = wceq 1289  wcel 1438
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081
This theorem is referenced by:  eqid  2088  sb8ab  2209  cbvab  2210  vjust  2620  nfccdeq  2836  difeqri  3118  uneqri  3140  incom  3190  ineqri  3191  difin  3234  invdif  3239  indif  3240  difundi  3249  indifdir  3253  pwv  3647  uniun  3667  intun  3714  intpr  3715  iuncom  3731  iuncom4  3732  iun0  3781  0iun  3782  iunin2  3788  iunun  3803  iunxun  3804  iunxiun  3805  iinpw  3811  inuni  3983  unidif0  3994  unipw  4035  snnex  4262  unon  4318  xpiundi  4484  xpiundir  4485  0xp  4506  iunxpf  4572  cnvuni  4610  dmiun  4633  dmuni  4634  epini  4790  rniun  4829  cnvresima  4907  imaco  4923  rnco  4924  dfmpt3  5122  imaiun  5521  opabex3d  5874  opabex3  5875  ecid  6335  qsid  6337  mapval2  6415  dfz2  8789  infssuzex  11038  1nprm  11189
  Copyright terms: Public domain W3C validator