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 ) ) |