![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > spcegv | GIF 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 2319 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1528 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | spcgv.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | spcegf 2820 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 = wceq 1353 ∃wex 1492 ∈ wcel 2148 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 |
This theorem is referenced by: spcedv 2826 spcev 2832 elabd 2882 eqeu 2907 absneu 3664 elunii 3814 axpweq 4170 euotd 4253 brcogw 4795 opeldmg 4831 breldmg 4832 dmsnopg 5099 dff3im 5660 elunirn 5764 unielxp 6172 op1steq 6177 tfr0dm 6320 tfrlemibxssdm 6325 tfrlemiex 6329 tfr1onlembxssdm 6341 tfr1onlemex 6345 tfrcllembxssdm 6354 tfrcllemex 6358 frecabcl 6397 ertr 6547 f1oen3g 6751 f1dom2g 6753 f1domg 6755 dom3d 6771 en1 6796 phpelm 6863 isinfinf 6894 ordiso 7032 djudom 7089 difinfsn 7096 ctm 7105 enumct 7111 djudoml 7215 djudomr 7216 cc2lem 7262 recexnq 7386 ltexprlemrl 7606 ltexprlemru 7608 recexprlemm 7620 recexprlemloc 7627 recexprlem1ssl 7629 recexprlem1ssu 7630 axpre-suploclemres 7897 frecuzrdgtcl 10407 frecuzrdgfunlem 10414 fihasheqf1oi 10760 zfz1isolem1 10813 climeu 11297 fsum3 11388 uzwodc 12030 eltg3 13428 uptx 13645 xblm 13788 bj-2inf 14550 subctctexmid 14610 |
Copyright terms: Public domain | W3C validator |