Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > spcegv | Structured version Visualization version 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 2764 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1843 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | spcgv.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | spcegf 3289 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1483 ∃wex 1704 ∈ wcel 1990 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 |
This theorem is referenced by: spcev 3300 elabd 3352 eqeu 3377 absneu 4263 issn 4363 elpreqprlem 4395 elunii 4441 axpweq 4842 brcogw 5290 opeldmd 5327 breldmg 5330 dmsnopg 5606 fvrnressn 6428 f1oexbi 7116 zfrep6 7134 unielxp 7204 wfrlem15 7429 ertr 7757 f1oen3g 7971 f1dom2g 7973 f1domg 7975 dom3d 7997 fodomr 8111 disjenex 8118 domssex2 8120 domssex 8121 ordiso 8421 fowdom 8476 brwdom2 8478 infeq5i 8533 oncard 8786 cardsn 8795 infxpenc2lem2 8843 dfac8b 8854 dfac8clem 8855 ac10ct 8857 ac5num 8859 acni2 8869 acnlem 8871 finnisoeu 8936 aceq3lem 8943 dfacacn 8963 infpss 9039 cflem 9068 cflecard 9075 cfslb 9088 cofsmo 9091 coftr 9095 alephsing 9098 fin4i 9120 axdc4lem 9277 ac6num 9301 axdclem2 9342 gchi 9446 grothpw 9648 hasheqf1oi 13140 hasheqf1oiOLD 13141 fz1isolem 13245 wrd2f1tovbij 13703 relexpindlem 13803 climeu 14286 fsum 14451 ntrivcvgn0 14630 fprod 14671 isacs1i 16318 mreacs 16319 brcici 16460 initoeu2lem2 16665 gsumval2a 17279 gsumval3lem2 18307 eltg3 20766 elptr 21376 uptx 21428 alexsubALTlem1 21851 ptcmplem3 21858 prdsxmslem2 22334 nbusgrf1o1 26272 cusgrexg 26340 cusgrfilem3 26353 sizusglecusg 26359 wlknwwlksnbij2 26778 wlkwwlkbij2 26785 wlksnwwlknvbij 26803 clwwlksbij 26920 clwwlksvbij 26922 numclwlk1lem2 27230 rmoeqALT 29327 aciunf1lem 29462 locfinref 29908 fnimage 32036 fnessref 32352 refssfne 32353 filnetlem4 32376 bj-restb 33047 fin2so 33396 unirep 33507 indexa 33528 rp-isfinite5 37863 nssd 39288 choicefi 39392 axccdom 39416 stoweidlem5 40222 stoweidlem27 40244 stoweidlem28 40245 stoweidlem31 40248 stoweidlem43 40260 stoweidlem44 40261 stoweidlem51 40268 stoweidlem59 40276 nsssmfmbflem 40986 sprbisymrel 41749 uspgrbisymrelALT 41763 irinitoringc 42069 |
Copyright terms: Public domain | W3C validator |