Description: Obsolete version of ceqsexv2d as of 5-Jun-2025. (Contributed by Thierry Arnoux, 10-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ceqsexv2dOLD.1 | |- A e. _V |
|
ceqsexv2dOLD.2 | |- ( x = A -> ( ph <-> ps ) ) |
||
ceqsexv2dOLD.3 | |- ps |
||
Assertion | ceqsexv2dOLD | |- E. x ph |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ceqsexv2dOLD.1 | |- A e. _V |
|
2 | ceqsexv2dOLD.2 | |- ( x = A -> ( ph <-> ps ) ) |
|
3 | ceqsexv2dOLD.3 | |- ps |
|
4 | 1 2 | ceqsexv | |- ( E. x ( x = A /\ ph ) <-> ps ) |
5 | 4 | biimpri | |- ( ps -> E. x ( x = A /\ ph ) ) |
6 | exsimpr | |- ( E. x ( x = A /\ ph ) -> E. x ph ) |
|
7 | 3 5 6 | mp2b | |- E. x ph |