| 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 3613 | 1 ⊢ (𝜑 → (𝜒 → ∃𝑥 ∈ 𝐵 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 |
| This theorem is referenced by: rspcebdv 3616 rspcev 3622 rspcedvd 3624 0csh0 14831 gcdcllem1 16536 nn0gsumfz 20002 pmatcollpw3lem 22789 pmatcollpw3fi1lem2 22793 pm2mpfo 22820 f1otrg 28879 cusgrfilem2 29474 wwlksnredwwlkn 29915 wwlksnextprop 29932 clwwlknun 30131 cusconngr 30210 xrofsup 32771 esum2d 34094 rexzrexnn0 42815 onsucelab 43276 ordnexbtwnsuc 43280 ov2ssiunov2 43713 requad2 47610 lcoel0 48345 lcoss 48353 el0ldep 48383 ldepspr 48390 islindeps2 48400 isldepslvec2 48402 affinecomb1 48623 isisod 48910 |
| Copyright terms: Public domain | W3C validator |