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.) |
Ref | Expression |
---|---|
spcedv.1 | ⊢ (𝜑 → 𝑋 ∈ V) |
spcedv.2 | ⊢ (𝜑 → 𝜒) |
spcedv.3 | ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
spcedv | ⊢ (𝜑 → ∃𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spcedv.1 | . 2 ⊢ (𝜑 → 𝑋 ∈ V) | |
2 | spcedv.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | spcedv.3 | . . 3 ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒)) | |
4 | 3 | spcegv 3597 | . 2 ⊢ (𝑋 ∈ V → (𝜒 → ∃𝑥𝜓)) |
5 | 1, 2, 4 | sylc 65 | 1 ⊢ (𝜑 → ∃𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1537 ∃wex 1780 ∈ wcel 2114 Vcvv 3494 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-cleq 2814 df-clel 2893 |
This theorem is referenced by: zfrep6 7656 wfrlem15 7969 ertr 8304 f1dom2g 8527 dom3d 8551 disjenex 8675 domssex2 8677 domssex 8678 brwdom2 9037 infxpenc2lem2 9446 dfac8clem 9458 ac5num 9462 acni2 9472 acnlem 9474 finnisoeu 9539 infpss 9639 cofsmo 9691 axdc4lem 9877 ac6num 9901 axdclem2 9942 hasheqf1od 13715 fz1isolem 13820 wrd2f1tovbij 14324 fsum 15077 ntrivcvgn0 15254 fprod 15295 setsexstruct2 16522 isacs1i 16928 mreacs 16929 gsumval3lem2 19026 eltg3 21570 elptr 22181 nbusgrf1o1 27152 cusgrexg 27226 cusgrfilem3 27239 sizusglecusg 27245 wwlksnextbij 27680 eqvreltr 35857 clrellem 40031 clcnvlem 40032 fundcmpsurinj 43618 prproropen 43719 isomgreqve 44039 isomushgr 44040 isomgrsym 44050 isomgrtr 44053 ushrisomgr 44055 uspgrsprfo 44072 uspgrbispr 44075 |
Copyright terms: Public domain | W3C validator |