|   | 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 2140, ax-11 2156. (Revised by Wolf Lammen, 25-Aug-2023.) | 
| Ref | Expression | 
|---|---|
| spcgv.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | 
| Ref | Expression | 
|---|---|
| spcegv | ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | elisset 2822 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) | |
| 2 | spcgv.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 3 | 2 | biimprcd 250 | . . 3 ⊢ (𝜓 → (𝑥 = 𝐴 → 𝜑)) | 
| 4 | 3 | eximdv 1916 | . 2 ⊢ (𝜓 → (∃𝑥 𝑥 = 𝐴 → ∃𝑥𝜑)) | 
| 5 | 1, 4 | syl5com 31 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1539 ∃wex 1778 ∈ wcel 2107 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-clel 2815 | 
| This theorem is referenced by: spcedv 3597 spcev 3605 eqeu 3711 absneu 4727 issn 4831 elpreqprlem 4865 elunii 4911 axpweq 5350 brcogw 5878 opeldmd 5916 breldmg 5919 dmsnopg 6232 predtrss 6342 fvrnressn 7180 f1oexbi 7951 unielxp 8053 frrlem13 8324 f1oen4g 9006 f1dom4g 9007 f1oen3g 9008 f1dom3g 9009 f1domg 9013 en2sn 9082 en2prd 9089 fodomr 9169 fodomfir 9369 ordiso 9557 fowdom 9612 inf0 9662 infeq5i 9677 oncard 10001 cardsn 10010 dfac8b 10072 ac10ct 10075 aceq3lem 10161 dfacacn 10183 cflem 10286 cflemOLD 10287 cflecard 10294 cfslb 10307 coftr 10314 alephsing 10317 fin4i 10339 axdc4lem 10496 gchi 10665 hasheqf1oi 14391 relexpindlem 15103 climeu 15592 brcici 17845 initoeu2lem2 18061 gsumval2a 18699 irinitoringc 21491 uptx 23634 alexsubALTlem1 24056 ptcmplem3 24063 prdsxmslem2 24543 tgjustf 28482 tgjustr 28483 wlksnwwlknvbij 29929 clwwlkvbij 30133 aciunf1lem 32673 locfinref 33841 fnimage 35931 fnessref 36359 refssfne 36360 filnetlem4 36383 bj-restb 37096 fin2so 37615 unirep 37722 indexa 37741 nssd 45115 choicefi 45210 axccdom 45232 stoweidlem5 46025 stoweidlem27 46047 stoweidlem28 46048 stoweidlem31 46051 stoweidlem43 46063 stoweidlem44 46064 stoweidlem51 46071 stoweidlem59 46079 nsssmfmbflem 46798 fundcmpsurinjpreimafv 47400 sprbisymrel 47491 uspgrbisymrelALT 48076 | 
| Copyright terms: Public domain | W3C validator |