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

Theorem eqriv 2034
 Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eqriv.1 (x Ax B)
Assertion
Ref Expression
eqriv A = B
Distinct variable groups:   x,A   x,B

Proof of Theorem eqriv
StepHypRef Expression
1 dfcleq 2031 . 2 (A = Bx(x Ax B))
2 eqriv.1 . 2 (x Ax B)
31, 2mpgbir 1339 1 A = B
 Colors of variables: wff set class Syntax hints:   ↔ wb 98   = wceq 1242   ∈ wcel 1390 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 1335  ax-ext 2019 This theorem depends on definitions:  df-bi 110  df-cleq 2030 This theorem is referenced by:  eqid  2037  sb8ab  2156  cbvab  2157  vjust  2552  nfccdeq  2756  difeqri  3058  uneqri  3079  incom  3123  ineqri  3124  difin  3168  invdif  3173  indif  3174  difundi  3183  indifdir  3187  pwv  3570  uniun  3590  intun  3637  intpr  3638  iuncom  3654  iuncom4  3655  iun0  3704  0iun  3705  iunin2  3711  iunun  3725  iunxun  3726  iunxiun  3727  iinpw  3733  inuni  3900  unidif0  3911  unipw  3944  snnex  4147  unon  4202  xpiundi  4341  xpiundir  4342  0xp  4363  iunxpf  4427  cnvuni  4464  dmiun  4487  dmuni  4488  epini  4639  rniun  4677  cnvresima  4753  imaco  4769  rnco  4770  dfmpt3  4964  imaiun  5342  opabex3d  5690  opabex3  5691  ecid  6105  qsid  6107  dfz2  8069
 Copyright terms: Public domain W3C validator