![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspcedv | Structured version Visualization version GIF version |
Description: Restricted existential specialization, using implicit substitution. (Contributed by FL, 17-Apr-2007.) (Revised by Mario Carneiro, 4-Jan-2017.) |
Ref | Expression |
---|---|
rspcdv.1 | ⊢ (𝜑 → 𝐴 ∈ 𝐵) |
rspcdv.2 | ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
rspcedv | ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspcdv.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵) | |
2 | rspcdv.2 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 2 | biimprd 247 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) |
4 | 1, 3 | rspcimedv 3603 | 1 ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ral 3062 df-rex 3071 |
This theorem is referenced by: rspcebdv 3606 rspcev 3612 rspcedvd 3614 0csh0 14742 gcdcllem1 16439 nn0gsumfz 19851 pmatcollpw3lem 22284 pmatcollpw3fi1lem2 22288 pm2mpfo 22315 f1otrg 28119 cusgrfilem2 28710 wwlksnredwwlkn 29146 wwlksnextprop 29163 clwwlknun 29362 cusconngr 29441 xrofsup 31975 esum2d 33086 rexzrexnn0 41532 onsucelab 42003 ordnexbtwnsuc 42007 ov2ssiunov2 42441 requad2 46281 lcoel0 47099 lcoss 47107 el0ldep 47137 ldepspr 47144 islindeps2 47154 isldepslvec2 47156 affinecomb1 47378 |
Copyright terms: Public domain | W3C validator |