![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspcedvdw | Structured version Visualization version GIF version |
Description: Version of rspcedvd 3613 where the implicit substitution hypothesis does not have an antecedent, which also avoids a disjoint variable condition on 𝜑, 𝑥. (Contributed by SN, 20-Aug-2024.) |
Ref | Expression |
---|---|
rspcedvdw.s | ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) |
rspcedvdw.1 | ⊢ (𝜑 → 𝐴 ∈ 𝐵) |
rspcedvdw.2 | ⊢ (𝜑 → 𝜒) |
Ref | Expression |
---|---|
rspcedvdw | ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspcedvdw.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵) | |
2 | rspcedvdw.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | rspcedvdw.s | . . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒)) | |
4 | 3 | rspcev 3611 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜒) → ∃𝑥 ∈ 𝐵 𝜓) |
5 | 1, 2, 4 | syl2anc 582 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 ∈ wcel 2098 ∃wrex 3067 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3059 df-rex 3068 |
This theorem is referenced by: opprring 20300 pzriprnglem7 21427 pzriprnglem13 21433 pzriprnglem14 21434 pzriprngALT 21435 remulscllem1 28256 remulscllem2 28257 fracerl 33025 fracfld 33027 idomsubr 33028 ghmqusnsglem1 33162 zringfrac 33285 ply1degltdimlem 33361 irredminply 33425 algextdeglem4 33429 algextdeglem8 33433 flt4lem2 42120 flt4lem7 42132 isuspgrim0lem 47265 |
Copyright terms: Public domain | W3C validator |