![]() |
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 14747 gcdcllem1 16444 nn0gsumfz 19893 pmatcollpw3lem 22505 pmatcollpw3fi1lem2 22509 pm2mpfo 22536 f1otrg 28377 cusgrfilem2 28968 wwlksnredwwlkn 29404 wwlksnextprop 29421 clwwlknun 29620 cusconngr 29699 xrofsup 32235 esum2d 33377 rexzrexnn0 41844 onsucelab 42315 ordnexbtwnsuc 42319 ov2ssiunov2 42753 requad2 46590 lcoel0 47197 lcoss 47205 el0ldep 47235 ldepspr 47242 islindeps2 47252 isldepslvec2 47254 affinecomb1 47476 |
Copyright terms: Public domain | W3C validator |