![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > abid | Unicode version |
Description: Simplification of class abstraction notation when the free and bound variables are identical. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
abid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-clab 2024 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sbid 1654 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitri 173 |
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 99 ax-ia2 100 ax-ia3 101 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-4 1397 ax-17 1416 ax-i9 1420 |
This theorem depends on definitions: df-bi 110 df-sb 1643 df-clab 2024 |
This theorem is referenced by: abeq2 2143 abeq2i 2145 abeq1i 2146 abeq2d 2147 abid2f 2199 elabgt 2678 elabgf 2679 ralab2 2699 rexab2 2701 sbccsbg 2872 sbccsb2g 2873 ss2ab 3002 abn0r 3237 tpid3g 3474 eluniab 3583 elintab 3617 iunab 3694 iinab 3709 intexabim 3897 iinexgm 3899 opm 3962 finds2 4267 dmmrnm 4497 sniota 4837 eusvobj2 5441 eloprabga 5533 indpi 6326 elabgf0 9251 |
Copyright terms: Public domain | W3C validator |