![]() |
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 248 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜒 → 𝜓)) |
4 | 1, 3 | rspcimedv 3612 | 1 ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1536 ∈ wcel 2105 ∃wrex 3067 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1539 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-ral 3059 df-rex 3068 |
This theorem is referenced by: rspcebdv 3615 rspcev 3621 rspcedvd 3623 0csh0 14827 gcdcllem1 16532 nn0gsumfz 20016 pmatcollpw3lem 22804 pmatcollpw3fi1lem2 22808 pm2mpfo 22835 f1otrg 28893 cusgrfilem2 29488 wwlksnredwwlkn 29924 wwlksnextprop 29941 clwwlknun 30140 cusconngr 30219 xrofsup 32777 esum2d 34073 rexzrexnn0 42791 onsucelab 43252 ordnexbtwnsuc 43256 ov2ssiunov2 43689 requad2 47547 lcoel0 48273 lcoss 48281 el0ldep 48311 ldepspr 48318 islindeps2 48328 isldepslvec2 48330 affinecomb1 48551 isisod 48806 |
Copyright terms: Public domain | W3C validator |