| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > spcedv | Structured version Visualization version GIF version | ||
| Description: Existential specialization, using implicit substitution, deduction version. (Contributed by RP, 12-Aug-2020.) (Revised by AV, 16-Aug-2024.) |
| Ref | Expression |
|---|---|
| spcedv.1 | ⊢ (𝜑 → 𝑋 ∈ 𝑉) |
| spcedv.2 | ⊢ (𝜑 → 𝜒) |
| spcedv.3 | ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| spcedv | ⊢ (𝜑 → ∃𝑥𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | spcedv.1 | . 2 ⊢ (𝜑 → 𝑋 ∈ 𝑉) | |
| 2 | spcedv.2 | . 2 ⊢ (𝜑 → 𝜒) | |
| 3 | spcedv.3 | . . 3 ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒)) | |
| 4 | 3 | spcegv 3597 | . 2 ⊢ (𝑋 ∈ 𝑉 → (𝜒 → ∃𝑥𝜓)) |
| 5 | 1, 2, 4 | sylc 65 | 1 ⊢ (𝜑 → ∃𝑥𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∃wex 1779 ∈ wcel 2108 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-clel 2816 |
| This theorem is referenced by: selsALT 5444 zfrep6 7979 wfrlem15OLD 8363 ertr 8760 dom3d 9034 disjenex 9175 domssex2 9177 domssex 9178 brwdom2 9613 infxpenc2lem2 10060 dfac8clem 10072 ac5num 10076 acni2 10086 acnlem 10088 finnisoeu 10153 infpss 10256 cofsmo 10309 axdc4lem 10495 ac6num 10519 axdclem2 10560 hasheqf1od 14392 fz1isolem 14500 wrd2f1tovbij 14999 fsum 15756 ntrivcvgn0 15934 fprod 15977 setsexstruct2 17212 isacs1i 17700 mreacs 17701 gsumval3lem2 19924 eltg3 22969 elptr 23581 nbusgrf1o1 29387 cusgrexg 29461 cusgrfilem3 29475 sizusglecusg 29481 wwlksnextbij 29922 gsumhashmul 33064 fzo0pmtrlast 33112 1arithidom 33565 gblacfnacd 35113 numiunnum 36471 bj-imdirco 37191 eqvreltr 38608 aks6d1c2 42131 sticksstones20 42167 onsucf1lem 43282 onsucf1olem 43283 nnoeomeqom 43325 rp-isfinite5 43530 clrellem 43635 clcnvlem 43636 fundcmpsurinj 47396 prproropen 47495 isuspgrim0 47872 grimidvtxedg 47876 grimcnv 47879 grimco 47880 gricushgr 47886 ushggricedg 47896 uhgrimisgrgric 47899 isgrtri 47910 usgrgrtrirex 47917 isubgr3stgrlem3 47935 isubgr3stgr 47942 uspgrlim 47959 grlimgrtri 47963 grlicref 47972 grlicsym 47973 grlictr 47975 uspgrsprfo 48064 uspgrbispr 48067 1aryenef 48566 2aryenef 48577 eufsnlem 48750 opncldeqv 48799 thincciso 49102 thinccisod 49103 functermceu 49142 mndtcbas 49178 |
| Copyright terms: Public domain | W3C validator |