NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  abid Unicode version

Theorem abid 2341
Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
abid

Proof of Theorem abid
StepHypRef Expression
1 df-clab 2340 . 2
2 sbid 1922 . 2
31, 2bitri 240 1
Colors of variables: wff setvar class
Syntax hints:   wb 176  wsb 1648   wcel 1710  cab 2339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649  df-clab 2340
This theorem is referenced by:  abeq2  2458  abeq2i  2460  abeq1i  2461  abeq2d  2462  abid2f  2514  elabgt  2982  elabgf  2983  ralab2  3001  rexab2  3003  sbccsbg  3164  sbccsb2g  3165  ss2ab  3334  abn0  3568  tpid3g  3831  eluniab  3903  elintab  3937  iunab  4012  iinab  4027  sniota  4369  eqop  4611  dfswap2  4741  eloprabga  5578
  Copyright terms: Public domain W3C validator