Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > spcev | Structured version Visualization version GIF version |
Description: Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) |
Ref | Expression |
---|---|
spcv.1 | ⊢ 𝐴 ∈ V |
spcv.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
spcev | ⊢ (𝜓 → ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spcv.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | spcv.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | spcegv 3267 | . 2 ⊢ (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑)) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ (𝜓 → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∃wex 1695 ∈ wcel 1977 Vcvv 3173 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 |
This theorem is referenced by: dtruALT 4826 elALT 4837 dtruALT2 4838 nnullss 4857 exss 4858 euotd 4900 opeldm 5250 elrnmpt1 5295 xpnz 5472 ssimaex 6173 fvelrn 6260 dff3 6280 exfo 6285 eufnfv 6395 elunirn 6413 fsnex 6438 f1prex 6439 foeqcnvco 6455 snnex 6862 ffoss 7020 op1steq 7101 frxp 7174 suppimacnv 7193 seqomlem2 7433 domtr 7895 ensn1 7906 en1 7909 enfixsn 7954 php3 8031 1sdom 8048 isinf 8058 ssfi 8065 ac6sfi 8089 hartogslem1 8330 brwdom2 8361 inf0 8401 axinf2 8420 cnfcom3clem 8485 tz9.1 8488 tz9.1c 8489 rankuni 8609 scott0 8632 cplem2 8636 bnd2 8639 karden 8641 cardprclem 8688 dfac4 8828 dfac5lem5 8833 dfac5 8834 dfac2a 8835 dfac2 8836 kmlem2 8856 kmlem13 8867 ackbij2 8948 cfsuc 8962 cfflb 8964 cfss 8970 cfsmolem 8975 cfcoflem 8977 fin23lem32 9049 axcc2lem 9141 axcc3 9143 axdc2lem 9153 axdc3lem2 9156 axcclem 9162 brdom3 9231 brdom7disj 9234 brdom6disj 9235 axpowndlem3 9300 canthnumlem 9349 canthp1lem2 9354 inar1 9476 recmulnq 9665 ltexnq 9676 halfnq 9677 ltbtwnnq 9679 1idpr 9730 ltexprlem7 9743 reclem2pr 9749 reclem3pr 9750 sup2 10858 nnunb 11165 uzrdgfni 12619 axdc4uzlem 12644 rtrclreclem3 13648 ntrivcvgmullem 14472 fprodntriv 14511 cnso 14815 vdwapun 15516 vdwlem1 15523 vdwlem12 15534 vdwlem13 15535 isacs2 16137 equivestrcsetc 16615 psgneu 17749 efglem 17952 lmisfree 20000 neitr 20794 cmpsublem 21012 cmpsub 21013 bwth 21023 1stcfb 21058 unisngl 21140 alexsubALTlem3 21663 alexsubALTlem4 21664 vitali 23188 mbfi1fseqlem6 23293 mbfi1flimlem 23295 aannenlem2 23888 istrkg2ld 25159 axlowdim 25641 padct 28885 cnvoprab 28886 f1ocnt 28946 locfinreflem 29235 locfinref 29236 prsdm 29288 prsrn 29289 eulerpart 29771 bnj150 30200 trpredpred 30972 fnsingle 31196 finminlem 31482 filnetlem3 31545 cnndvlem2 31699 bj-restpw 32226 bj-rest0 32227 bj-toprntopon 32244 poimirlem2 32581 mblfinlem3 32618 mblfinlem4 32619 ismblfin 32620 itg2addnclem 32631 itg2addnc 32634 indexdom 32699 sdclem2 32708 fdc 32711 prtlem16 33172 dihglblem2aN 35600 eldioph2lem2 36342 dford3lem2 36612 aomclem7 36648 dfac11 36650 relintabex 36906 rclexi 36941 trclexi 36946 rtrclexi 36947 fnchoice 38211 ssnnf1octb 38377 fzisoeu 38455 stoweidlem28 38921 nnfoctbdjlem 39348 1wlkpwwlkf1ouspgr 41076 1wlkisowwlkupgr 41077 setrec1lem3 42235 setrec2lem2 42240 |
Copyright terms: Public domain | W3C validator |