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.) (Revised by AV, 16-Aug-2024.) |
Ref | Expression |
---|---|
spcedv.1 | ⊢ (𝜑 → 𝑋 ∈ 𝑉) |
spcedv.2 | ⊢ (𝜑 → 𝜒) |
spcedv.3 | ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
spcedv | ⊢ (𝜑 → ∃𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spcedv.1 | . 2 ⊢ (𝜑 → 𝑋 ∈ 𝑉) | |
2 | spcedv.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | spcedv.3 | . . 3 ⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒)) | |
4 | 3 | spcegv 3545 | . 2 ⊢ (𝑋 ∈ 𝑉 → (𝜒 → ∃𝑥𝜓)) |
5 | 1, 2, 4 | sylc 65 | 1 ⊢ (𝜑 → ∃𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1540 ∃wex 1780 ∈ wcel 2105 |
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 1912 ax-6 1970 ax-7 2010 ax-8 2107 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2714 df-clel 2814 |
This theorem is referenced by: selsALT 5384 zfrep6 7865 wfrlem15OLD 8224 ertr 8584 f1dom2gOLD 8831 dom3d 8855 disjenex 9000 domssex2 9002 domssex 9003 brwdom2 9430 infxpenc2lem2 9877 dfac8clem 9889 ac5num 9893 acni2 9903 acnlem 9905 finnisoeu 9970 infpss 10074 cofsmo 10126 axdc4lem 10312 ac6num 10336 axdclem2 10377 hasheqf1od 14168 fz1isolem 14275 wrd2f1tovbij 14774 fsum 15531 ntrivcvgn0 15709 fprod 15750 setsexstruct2 16973 isacs1i 17463 mreacs 17464 gsumval3lem2 19602 eltg3 22218 elptr 22830 nbusgrf1o1 28026 cusgrexg 28100 cusgrfilem3 28113 sizusglecusg 28119 wwlksnextbij 28555 gsumhashmul 31603 bj-imdirco 35474 eqvreltr 36882 sticksstones20 40387 rp-isfinite5 41454 clrellem 41559 clcnvlem 41560 fundcmpsurinj 45220 prproropen 45319 isomgreqve 45636 isomushgr 45637 isomgrsym 45647 isomgrtr 45650 ushrisomgr 45652 uspgrsprfo 45669 uspgrbispr 45672 1aryenef 46350 2aryenef 46361 eufsnlem 46527 opncldeqv 46554 thincciso 46689 mndtcbas 46727 |
Copyright terms: Public domain | W3C validator |