![]() |
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 2229 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1467 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | spcgv.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | spcegf 2703 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1290 ∃wex 1427 ∈ wcel 1439 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-v 2622 |
This theorem is referenced by: spcev 2714 eqeu 2786 absneu 3518 elunii 3664 axpweq 4012 euotd 4090 brcogw 4618 opeldmg 4654 breldmg 4655 dmsnopg 4915 dff3im 5458 elunirn 5559 unielxp 5958 op1steq 5963 tfr0dm 6101 tfrlemibxssdm 6106 tfrlemiex 6110 tfr1onlembxssdm 6122 tfr1onlemex 6126 tfrcllembxssdm 6135 tfrcllemex 6139 frecabcl 6178 ertr 6321 f1oen3g 6525 f1dom2g 6527 f1domg 6529 dom3d 6545 en1 6570 phpelm 6636 isinfinf 6667 ordiso 6783 djudom 6837 ctm 6845 enumct 6847 recexnq 7010 ltexprlemrl 7230 ltexprlemru 7232 recexprlemm 7244 recexprlemloc 7251 recexprlem1ssl 7253 recexprlem1ssu 7254 frecuzrdgtcl 9880 frecuzrdgfunlem 9887 fihasheqf1oi 10257 zfz1isolem1 10306 climeu 10745 fisum 10839 eltg3 11818 bj-2inf 12106 |
Copyright terms: Public domain | W3C validator |