Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > spcegv | Unicode version |
Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
spcgv.1 |
Ref | Expression |
---|---|
spcegv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2312 | . 2 | |
2 | nfv 1521 | . 2 | |
3 | spcgv.1 | . 2 | |
4 | 1, 2, 3 | spcegf 2813 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1348 wex 1485 wcel 2141 |
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-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-v 2732 |
This theorem is referenced by: spcedv 2819 spcev 2825 elabd 2875 eqeu 2900 absneu 3655 elunii 3801 axpweq 4157 euotd 4239 brcogw 4780 opeldmg 4816 breldmg 4817 dmsnopg 5082 dff3im 5641 elunirn 5745 unielxp 6153 op1steq 6158 tfr0dm 6301 tfrlemibxssdm 6306 tfrlemiex 6310 tfr1onlembxssdm 6322 tfr1onlemex 6326 tfrcllembxssdm 6335 tfrcllemex 6339 frecabcl 6378 ertr 6528 f1oen3g 6732 f1dom2g 6734 f1domg 6736 dom3d 6752 en1 6777 phpelm 6844 isinfinf 6875 ordiso 7013 djudom 7070 difinfsn 7077 ctm 7086 enumct 7092 djudoml 7196 djudomr 7197 cc2lem 7228 recexnq 7352 ltexprlemrl 7572 ltexprlemru 7574 recexprlemm 7586 recexprlemloc 7593 recexprlem1ssl 7595 recexprlem1ssu 7596 axpre-suploclemres 7863 frecuzrdgtcl 10368 frecuzrdgfunlem 10375 fihasheqf1oi 10722 zfz1isolem1 10775 climeu 11259 fsum3 11350 uzwodc 11992 eltg3 12851 uptx 13068 xblm 13211 bj-2inf 13973 subctctexmid 14034 |
Copyright terms: Public domain | W3C validator |