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.) Avoid ax-10 2141, ax-11 2158. (Revised by Wolf Lammen, 25-Aug-2023.) |
Ref | Expression |
---|---|
spcgv.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
spcegv | ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 2819 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | spcgv.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | biimprcd 253 | . . 3 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑)) |
4 | 3 | eximdv 1925 | . 2 ⊢ (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑)) |
5 | 1, 4 | syl5com 31 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1543 ∃wex 1787 ∈ wcel 2110 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-clel 2816 |
This theorem is referenced by: spcedv 3513 spcev 3521 eqeu 3619 absneu 4644 issn 4743 elpreqprlem 4776 elunii 4824 axpweq 5257 brcogw 5737 opeldmd 5775 breldmg 5778 dmsnopg 6076 fvrnressn 6976 f1oexbi 7706 unielxp 7799 frrlem13 8039 f1oen3g 8644 f1domg 8648 en2sn 8718 en2snOLD 8719 fodomr 8797 ordiso 9132 fowdom 9187 inf0 9236 infeq5i 9251 oncard 9576 cardsn 9585 dfac8b 9645 ac10ct 9648 aceq3lem 9734 dfacacn 9755 cflem 9860 cflecard 9867 cfslb 9880 coftr 9887 alephsing 9890 fin4i 9912 axdc4lem 10069 gchi 10238 hasheqf1oi 13918 relexpindlem 14626 climeu 15116 brcici 17305 initoeu2lem2 17521 gsumval2a 18157 uptx 22522 alexsubALTlem1 22944 ptcmplem3 22951 prdsxmslem2 23427 tgjustf 26564 tgjustr 26565 wlksnwwlknvbij 27992 clwwlkvbij 28196 aciunf1lem 30719 locfinref 31505 fnimage 33968 fnessref 34283 refssfne 34284 filnetlem4 34307 bj-restb 35000 fin2so 35501 unirep 35608 indexa 35628 rp-isfinite5 40809 nssd 42328 choicefi 42413 axccdom 42435 stoweidlem5 43221 stoweidlem27 43243 stoweidlem28 43244 stoweidlem31 43247 stoweidlem43 43259 stoweidlem44 43260 stoweidlem51 43267 stoweidlem59 43275 nsssmfmbflem 43985 fundcmpsurinjpreimafv 44533 sprbisymrel 44624 isomuspgrlem2 44958 uspgrbisymrelALT 44990 irinitoringc 45300 |
Copyright terms: Public domain | W3C validator |