![]() |
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 2079, ax-11 2093. (Revised by Wolf Lammen, 25-Aug-2023.) |
Ref | Expression |
---|---|
spcgv.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
spcegv | ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 3426 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | spcgv.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | biimprcd 242 | . . 3 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑)) |
4 | 3 | eximdv 1876 | . 2 ⊢ (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑)) |
5 | 1, 4 | syl5com 31 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1507 ∃wex 1742 ∈ wcel 2050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2771 df-clel 2846 |
This theorem is referenced by: spcev 3525 elabd 3583 eqeu 3611 absneu 4539 issn 4638 elpreqprlem 4671 elunii 4718 axpweq 5119 brcogw 5590 opeldmd 5626 breldmg 5629 dmsnopg 5911 fvrnressn 6748 f1oexbi 7450 unielxp 7541 f1oen3g 8324 f1domg 8328 fodomr 8466 ordiso 8777 fowdom 8832 infeq5i 8895 oncard 9185 cardsn 9194 dfac8b 9253 ac10ct 9256 aceq3lem 9342 dfacacn 9363 cflem 9468 cflecard 9475 cfslb 9488 coftr 9495 alephsing 9498 fin4i 9520 axdc4lem 9677 gchi 9846 hasheqf1oi 13530 relexpindlem 14286 climeu 14776 brcici 16931 initoeu2lem2 17136 gsumval2a 17750 uptx 21940 alexsubALTlem1 22362 ptcmplem3 22369 prdsxmslem2 22845 tgjustf 25964 tgjustr 25965 wlksnwwlknvbij 27411 clwwlkvbij 27644 clwwlkvbijOLD 27645 aciunf1lem 30172 locfinref 30749 frrlem13 32656 fnimage 32911 fnessref 33226 refssfne 33227 filnetlem4 33250 bj-restb 33895 fin2so 34320 unirep 34430 indexa 34450 rp-isfinite5 39279 nssd 40795 choicefi 40889 axccdom 40913 stoweidlem5 41722 stoweidlem27 41744 stoweidlem28 41745 stoweidlem31 41748 stoweidlem43 41760 stoweidlem44 41761 stoweidlem51 41768 stoweidlem59 41776 nsssmfmbflem 42486 sprbisymrel 43030 isomuspgrlem2 43367 uspgrbisymrelALT 43399 irinitoringc 43705 |
Copyright terms: Public domain | W3C validator |