![]() |
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 2821 | 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 2740 |
This theorem is referenced by: spcedv 2827 spcev 2833 elabd 2883 eqeu 2908 absneu 3665 elunii 3815 axpweq 4172 euotd 4255 brcogw 4797 opeldmg 4833 breldmg 4834 dmsnopg 5101 dff3im 5662 elunirn 5767 unielxp 6175 op1steq 6180 tfr0dm 6323 tfrlemibxssdm 6328 tfrlemiex 6332 tfr1onlembxssdm 6344 tfr1onlemex 6348 tfrcllembxssdm 6357 tfrcllemex 6361 frecabcl 6400 ertr 6550 f1oen3g 6754 f1dom2g 6756 f1domg 6758 dom3d 6774 en1 6799 phpelm 6866 isinfinf 6897 ordiso 7035 djudom 7092 difinfsn 7099 ctm 7108 enumct 7114 djudoml 7218 djudomr 7219 cc2lem 7265 recexnq 7389 ltexprlemrl 7609 ltexprlemru 7611 recexprlemm 7623 recexprlemloc 7630 recexprlem1ssl 7632 recexprlem1ssu 7633 axpre-suploclemres 7900 frecuzrdgtcl 10412 frecuzrdgfunlem 10419 fihasheqf1oi 10767 zfz1isolem1 10820 climeu 11304 fsum3 11395 uzwodc 12038 eltg3 13560 uptx 13777 xblm 13920 bj-2inf 14693 subctctexmid 14753 |
Copyright terms: Public domain | W3C validator |