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

Theorem eqriv 2019
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 2016 . 2 (A = Bx(x Ax B))
2 eqriv.1 . 2 (x Ax B)
31, 2mpgbir 1322 1 A = B
Colors of variables: wff set class
Syntax hints:  wb 98   = wceq 1228   wcel 1374
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 1318  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  eqid  2022  sb8ab  2141  cbvab  2142  vjust  2534  nfccdeq  2737  difeqri  3039  uneqri  3060  incom  3104  ineqri  3105  difin  3149  invdif  3154  indif  3155  difundi  3164  indifdir  3168  pwv  3551  uniun  3571  intun  3618  intpr  3619  iuncom  3635  iuncom4  3636  iun0  3685  0iun  3686  iunin2  3692  iunun  3706  iunxun  3707  iunxiun  3708  iinpw  3714  inuni  3881  unidif0  3892  unipw  3925  snnex  4129  unon  4184  xpiundi  4323  xpiundir  4324  0xp  4345  iunxpf  4409  cnvuni  4446  dmiun  4469  dmuni  4470  epini  4621  rniun  4659  cnvresima  4735  imaco  4751  rnco  4752  dfmpt3  4945  imaiun  5322  opabex3d  5669  opabex3  5670  ecid  6078  qsid  6080
  Copyright terms: Public domain W3C validator