![]() |
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 2282 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1509 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | spcgv.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | spcegf 2772 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1332 ∃wex 1469 ∈ wcel 1481 |
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 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-v 2691 |
This theorem is referenced by: spcedv 2778 spcev 2784 elabd 2833 eqeu 2858 absneu 3603 elunii 3749 axpweq 4103 euotd 4184 brcogw 4716 opeldmg 4752 breldmg 4753 dmsnopg 5018 dff3im 5573 elunirn 5675 unielxp 6080 op1steq 6085 tfr0dm 6227 tfrlemibxssdm 6232 tfrlemiex 6236 tfr1onlembxssdm 6248 tfr1onlemex 6252 tfrcllembxssdm 6261 tfrcllemex 6265 frecabcl 6304 ertr 6452 f1oen3g 6656 f1dom2g 6658 f1domg 6660 dom3d 6676 en1 6701 phpelm 6768 isinfinf 6799 ordiso 6929 djudom 6986 difinfsn 6993 ctm 7002 enumct 7008 djudoml 7092 djudomr 7093 cc2lem 7098 recexnq 7222 ltexprlemrl 7442 ltexprlemru 7444 recexprlemm 7456 recexprlemloc 7463 recexprlem1ssl 7465 recexprlem1ssu 7466 axpre-suploclemres 7733 frecuzrdgtcl 10216 frecuzrdgfunlem 10223 fihasheqf1oi 10566 zfz1isolem1 10615 climeu 11097 fsum3 11188 eltg3 12265 uptx 12482 xblm 12625 bj-2inf 13307 subctctexmid 13369 |
Copyright terms: Public domain | W3C validator |