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 2279 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1508 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | spcgv.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | spcegf 2764 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1331 ∃wex 1468 ∈ wcel 1480 |
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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-v 2683 |
This theorem is referenced by: spcev 2775 elabd 2824 eqeu 2849 absneu 3590 elunii 3736 axpweq 4090 euotd 4171 brcogw 4703 opeldmg 4739 breldmg 4740 dmsnopg 5005 dff3im 5558 elunirn 5660 unielxp 6065 op1steq 6070 tfr0dm 6212 tfrlemibxssdm 6217 tfrlemiex 6221 tfr1onlembxssdm 6233 tfr1onlemex 6237 tfrcllembxssdm 6246 tfrcllemex 6250 frecabcl 6289 ertr 6437 f1oen3g 6641 f1dom2g 6643 f1domg 6645 dom3d 6661 en1 6686 phpelm 6753 isinfinf 6784 ordiso 6914 djudom 6971 difinfsn 6978 ctm 6987 enumct 6993 djudoml 7068 djudomr 7069 recexnq 7191 ltexprlemrl 7411 ltexprlemru 7413 recexprlemm 7425 recexprlemloc 7432 recexprlem1ssl 7434 recexprlem1ssu 7435 axpre-suploclemres 7702 frecuzrdgtcl 10178 frecuzrdgfunlem 10185 fihasheqf1oi 10527 zfz1isolem1 10576 climeu 11058 fsum3 11149 eltg3 12215 uptx 12432 xblm 12575 bj-2inf 13125 subctctexmid 13185 |
Copyright terms: Public domain | W3C validator |