Description: Membership in class intersection. (Contributed by NM, 14-Oct-1999) (Proof shortened by Andrew Salmon, 9-Jul-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | elinti | |- ( A e. |^| B -> ( C e. B -> A e. C ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elintg | |- ( A e. |^| B -> ( A e. |^| B <-> A. x e. B A e. x ) ) |
|
2 | eleq2 | |- ( x = C -> ( A e. x <-> A e. C ) ) |
|
3 | 2 | rspccv | |- ( A. x e. B A e. x -> ( C e. B -> A e. C ) ) |
4 | 1 3 | syl6bi | |- ( A e. |^| B -> ( A e. |^| B -> ( C e. B -> A e. C ) ) ) |
5 | 4 | pm2.43i | |- ( A e. |^| B -> ( C e. B -> A e. C ) ) |