![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sp | Unicode version |
Description: Specialization. Another name for ax-4 1510. (Contributed by NM, 21-May-2008.) |
Ref | Expression |
---|---|
sp |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-4 1510 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-4 1510 |
This theorem is referenced by: axi12 1514 nfr 1518 sps 1537 spsd 1538 19.3 1554 cbv1h 1746 nfald 1760 dveeq2 1815 nfsbxy 1942 nfsbxyt 1943 nfcr 2311 nfabdw 2338 rsp 2524 ceqex 2864 abidnf 2905 mob2 2917 csbie2t 3105 sbcnestgf 3108 mpteq12f 4082 dtruarb 4190 copsex2t 4244 ssopab2 4274 eusv1 4451 alxfr 4460 eunex 4559 iota1 5191 fiintim 6925 genprndl 7517 genprndu 7518 fiinopn 13373 bdel 14457 bdsepnft 14499 strcollnft 14596 |
Copyright terms: Public domain | W3C validator |