Description: Version of rspcedvd where the implicit substitution hypothesis does not have an antecedent, which also avoids a disjoint variable condition on ph , x . (Contributed by SN, 20-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rspcedvdw.s | |- ( x = A -> ( ps <-> ch ) ) |
|
rspcedvdw.1 | |- ( ph -> A e. B ) |
||
rspcedvdw.2 | |- ( ph -> ch ) |
||
Assertion | rspcedvdw | |- ( ph -> E. x e. B ps ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspcedvdw.s | |- ( x = A -> ( ps <-> ch ) ) |
|
2 | rspcedvdw.1 | |- ( ph -> A e. B ) |
|
3 | rspcedvdw.2 | |- ( ph -> ch ) |
|
4 | 1 | rspcev | |- ( ( A e. B /\ ch ) -> E. x e. B ps ) |
5 | 2 3 4 | syl2anc | |- ( ph -> E. x e. B ps ) |