Description: Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003) (Proof shortened by JJ, 26-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elintg | |- ( A e. V -> ( A e. |^| B <-> A. x e. B A e. x ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elequ1 | |- ( z = y -> ( z e. x <-> y e. x ) ) |
|
| 2 | 1 | ralbidv | |- ( z = y -> ( A. x e. B z e. x <-> A. x e. B y e. x ) ) |
| 3 | eleq1 | |- ( y = A -> ( y e. x <-> A e. x ) ) |
|
| 4 | 3 | ralbidv | |- ( y = A -> ( A. x e. B y e. x <-> A. x e. B A e. x ) ) |
| 5 | dfint2 | |- |^| B = { z | A. x e. B z e. x } |
|
| 6 | 2 4 5 | elab2gw | |- ( A e. V -> ( A e. |^| B <-> A. x e. B A e. x ) ) |