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 | eleq1 | |- ( y = A -> ( y e. x <-> A e. x ) ) |
|
| 2 | 1 | ralbidv | |- ( y = A -> ( A. x e. B y e. x <-> A. x e. B A e. x ) ) |
| 3 | dfint2 | |- |^| B = { y | A. x e. B y e. x } |
|
| 4 | 2 3 | elab2g | |- ( A e. V -> ( A e. |^| B <-> A. x e. B A e. x ) ) |