![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > abeq2i | Unicode version |
Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.) |
Ref | Expression |
---|---|
abeqi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
abeq2i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abeqi.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eleq2i 2179 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | abid 2101 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | bitri 183 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-ext 2095 |
This theorem depends on definitions: df-bi 116 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 |
This theorem is referenced by: rabid 2578 vex 2658 csbco 2978 csbnestgf 3016 ifmdc 3473 pwss 3490 snsspw 3655 iunpw 4359 ordon 4360 funcnv3 5141 tfrlem4 6162 tfrlem8 6167 tfrlem9 6168 tfrlemibxssdm 6176 tfr1onlembxssdm 6192 tfrcllembxssdm 6205 ixpm 6576 mapsnen 6657 sbthlem1 6795 1idprl 7340 1idpru 7341 recexprlem1ssl 7383 recexprlem1ssu 7384 recexprlemss1l 7385 recexprlemss1u 7386 txbas 12263 |
Copyright terms: Public domain | W3C validator |