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

Theorem eqriv 2020
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 2017 . 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 1375
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 2005
This theorem depends on definitions:  df-bi 110  df-cleq 2016
This theorem is referenced by:  eqid  2023  sb8ab  2142  cbvab  2143  vjust  2535  nfccdeq  2738  difeqri  3040  uneqri  3061  incom  3105  ineqri  3106  difin  3150  invdif  3155  indif  3156  difundi  3165  indifdir  3169  pwv  3552  uniun  3572  intun  3619  intpr  3620  iuncom  3636  iuncom4  3637  iun0  3686  0iun  3687  iunin2  3693  iunun  3707  iunxun  3708  iunxiun  3709  iinpw  3715  inuni  3882  unidif0  3893  unipw  3926  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  5668  opabex3  5669  ecid  6074  qsid  6075
  Copyright terms: Public domain W3C validator