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

Theorem abeq2i 2265
 Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.)
Hypothesis
Ref Expression
abeqi.1
Assertion
Ref Expression
abeq2i

Proof of Theorem abeq2i
StepHypRef Expression
1 abeqi.1 . . 3
21eleq2i 2221 . 2
3 abid 2142 . 2
42, 3bitri 183 1
 Colors of variables: wff set class Syntax hints:   wb 104   wceq 1332   wcel 2125  cab 2140 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-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-ext 2136 This theorem depends on definitions:  df-bi 116  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150 This theorem is referenced by:  rabid  2629  vex  2712  csbco  3037  csbcow  3038  csbnestgf  3079  ifmdc  3538  pwss  3555  snsspw  3723  iunpw  4434  ordon  4439  funcnv3  5225  tfrlem4  6250  tfrlem8  6255  tfrlem9  6256  tfrlemibxssdm  6264  tfr1onlembxssdm  6280  tfrcllembxssdm  6293  ixpm  6664  mapsnen  6745  sbthlem1  6890  1idprl  7489  1idpru  7490  recexprlem1ssl  7532  recexprlem1ssu  7533  recexprlemss1l  7534  recexprlemss1u  7535  txbas  12597
 Copyright terms: Public domain W3C validator