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 2126 | . 2 | |
2 | sbid 1747 | . 2 | |
3 | 1, 2 | bitri 183 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wcel 1480 wsb 1735 cab 2125 |
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-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-4 1487 ax-17 1506 ax-i9 1510 |
This theorem depends on definitions: df-bi 116 df-sb 1736 df-clab 2126 |
This theorem is referenced by: abeq2 2248 abeq2i 2250 abeq1i 2251 abeq2d 2252 abid2f 2306 elabgt 2825 elabgf 2826 ralab2 2848 rexab2 2850 sbccsbg 3031 sbccsb2g 3032 ss2ab 3165 abn0r 3387 abn0m 3388 tpid3g 3638 eluniab 3748 elintab 3782 iunab 3859 iinab 3874 intexabim 4077 iinexgm 4079 opm 4156 finds2 4515 dmmrnm 4758 sniota 5115 eusvobj2 5760 eloprabga 5858 indpi 7150 elabgf0 12984 |
Copyright terms: Public domain | W3C validator |