![]() |
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 2129, ax-11 2146. (Revised by Wolf Lammen, 25-Aug-2023.) |
Ref | Expression |
---|---|
spcgv.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
spcegv | ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elisset 2807 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
2 | spcgv.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 2 | biimprcd 249 | . . 3 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑)) |
4 | 3 | eximdv 1912 | . 2 ⊢ (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑)) |
5 | 1, 4 | syl5com 31 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 ∃wex 1773 ∈ wcel 2098 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-clel 2802 |
This theorem is referenced by: spcedv 3582 spcev 3590 eqeu 3698 absneu 4734 issn 4835 elpreqprlem 4868 elunii 4914 axpweq 5350 brcogw 5871 opeldmd 5909 breldmg 5912 dmsnopg 6219 predtrss 6330 fvrnressn 7170 f1oexbi 7936 unielxp 8032 frrlem13 8304 f1oen4g 8985 f1dom4g 8986 f1oen3g 8987 f1dom3g 8988 f1domg 8993 en2sn 9067 en2snOLD 9068 en2prd 9076 fodomr 9156 ordiso 9546 fowdom 9601 inf0 9651 infeq5i 9666 oncard 9990 cardsn 9999 dfac8b 10061 ac10ct 10064 aceq3lem 10150 dfacacn 10171 cflem 10276 cflecard 10283 cfslb 10296 coftr 10303 alephsing 10306 fin4i 10328 axdc4lem 10485 gchi 10654 hasheqf1oi 14354 relexpindlem 15054 climeu 15543 brcici 17802 initoeu2lem2 18023 gsumval2a 18664 irinitoringc 21439 uptx 23590 alexsubALTlem1 24012 ptcmplem3 24019 prdsxmslem2 24499 tgjustf 28369 tgjustr 28370 wlksnwwlknvbij 29811 clwwlkvbij 30015 aciunf1lem 32549 locfinref 33593 fnimage 35676 fnessref 35992 refssfne 35993 filnetlem4 36016 bj-restb 36724 fin2so 37231 unirep 37338 indexa 37357 nssd 44616 choicefi 44717 axccdom 44739 stoweidlem5 45536 stoweidlem27 45558 stoweidlem28 45559 stoweidlem31 45562 stoweidlem43 45574 stoweidlem44 45575 stoweidlem51 45582 stoweidlem59 45590 nsssmfmbflem 46309 fundcmpsurinjpreimafv 46890 sprbisymrel 46981 uspgrbisymrelALT 47408 |
Copyright terms: Public domain | W3C validator |