Description: Alternate elimitation of a restricted existential quantifier, using implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ceqsrexv2.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
Assertion | ceqsrexv2 | |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ceqsrexv2.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
2 | 1 | ceqsrexbv | |- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) ) |