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 2258 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1493 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | spcgv.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | spcegf 2743 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1316 ∃wex 1453 ∈ wcel 1465 |
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 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-v 2662 |
This theorem is referenced by: spcev 2754 eqeu 2827 absneu 3565 elunii 3711 axpweq 4065 euotd 4146 brcogw 4678 opeldmg 4714 breldmg 4715 dmsnopg 4980 dff3im 5533 elunirn 5635 unielxp 6040 op1steq 6045 tfr0dm 6187 tfrlemibxssdm 6192 tfrlemiex 6196 tfr1onlembxssdm 6208 tfr1onlemex 6212 tfrcllembxssdm 6221 tfrcllemex 6225 frecabcl 6264 ertr 6412 f1oen3g 6616 f1dom2g 6618 f1domg 6620 dom3d 6636 en1 6661 phpelm 6728 isinfinf 6759 ordiso 6889 djudom 6946 difinfsn 6953 ctm 6962 enumct 6968 djudoml 7043 djudomr 7044 recexnq 7166 ltexprlemrl 7386 ltexprlemru 7388 recexprlemm 7400 recexprlemloc 7407 recexprlem1ssl 7409 recexprlem1ssu 7410 axpre-suploclemres 7677 frecuzrdgtcl 10153 frecuzrdgfunlem 10160 fihasheqf1oi 10502 zfz1isolem1 10551 climeu 11033 fsum3 11124 eltg3 12153 uptx 12370 xblm 12513 bj-2inf 13063 subctctexmid 13123 |
Copyright terms: Public domain | W3C validator |