Description: Membership in indexed intersection. See eliincex for a counterexample showing that the precondition B =/= (/) cannot be simply dropped. eliin uses an alternative precondition (and it doesn't have a disjoint var constraint between B and x ; see eliin2f ). (Contributed by Glauco Siliprandi, 26-Jun-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | eliin2 | |- ( B =/= (/) -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfcv | |- F/_ x B |
|
| 2 | 1 | eliin2f | |- ( B =/= (/) -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) ) |