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

Theorem eqriv 2136
 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 2133 . 2 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
2 eqriv.1 . 2 (𝑥𝐴𝑥𝐵)
31, 2mpgbir 1429 1 𝐴 = 𝐵
 Colors of variables: wff set class Syntax hints:   ↔ wb 104   = wceq 1331   ∈ wcel 1480 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-cleq 2132 This theorem is referenced by:  eqid  2139  sb8ab  2261  cbvabw  2262  cbvab  2263  vjust  2687  nfccdeq  2907  difeqri  3196  uneqri  3218  incom  3268  ineqri  3269  difin  3313  invdif  3318  indif  3319  difundi  3328  indifdir  3332  pwv  3735  uniun  3755  intun  3802  intpr  3803  iuncom  3819  iuncom4  3820  iun0  3869  0iun  3870  iunin2  3876  iunun  3891  iunxun  3892  iunxiun  3894  iinpw  3903  inuni  4080  unidif0  4091  unipw  4139  snnex  4369  unon  4427  xpiundi  4597  xpiundir  4598  0xp  4619  iunxpf  4687  cnvuni  4725  dmiun  4748  dmuni  4749  epini  4910  rniun  4949  cnvresima  5028  imaco  5044  rnco  5045  dfmpt3  5245  imaiun  5661  opabex3d  6019  opabex3  6020  ecid  6492  qsid  6494  mapval2  6572  ixpin  6617  dfz2  9137  infssuzex  11655  1nprm  11808
 Copyright terms: Public domain W3C validator