Description: Membership in a class abstraction, with a weaker antecedent than elabg . (Contributed by NM, 29-Aug-2006)
Ref | Expression | ||
---|---|---|---|
Hypothesis | elab3g.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
Assertion | elab3g | |- ( ( ps -> A e. B ) -> ( A e. { x | ph } <-> ps ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elab3g.1 | |- ( x = A -> ( ph <-> ps ) ) |
|
2 | nfcv | |- F/_ x A |
|
3 | nfv | |- F/ x ps |
|
4 | 2 3 1 | elab3gf | |- ( ( ps -> A e. B ) -> ( A e. { x | ph } <-> ps ) ) |