Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sp | Unicode version |
Description: Specialization. Another name for ax-4 1497. (Contributed by NM, 21-May-2008.) |
Ref | Expression |
---|---|
sp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-4 1497 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wal 1340 |
This theorem was proved from axioms: ax-4 1497 |
This theorem is referenced by: axi12 1501 nfr 1505 sps 1524 spsd 1525 19.3 1541 cbv1h 1733 nfald 1747 dveeq2 1802 nfsbxy 1929 nfsbxyt 1930 nfcr 2298 nfabdw 2325 rsp 2511 ceqex 2848 abidnf 2889 mob2 2901 csbie2t 3088 sbcnestgf 3091 mpteq12f 4056 dtruarb 4164 copsex2t 4217 ssopab2 4247 eusv1 4424 alxfr 4433 eunex 4532 iota1 5161 fiintim 6885 genprndl 7453 genprndu 7454 fiinopn 12549 bdel 13568 bdsepnft 13610 strcollnft 13707 |
Copyright terms: Public domain | W3C validator |