Description: Bound-variable hypothesis builder for indexed intersection. (Contributed by Mario Carneiro, 25-Jan-2014) Add disjoint variable condition to avoid ax-13 . See nfiing for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | nfiun.1 | |- F/_ y A |
|
| nfiun.2 | |- F/_ y B |
||
| Assertion | nfiin | |- F/_ y |^|_ x e. A B |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfiun.1 | |- F/_ y A |
|
| 2 | nfiun.2 | |- F/_ y B |
|
| 3 | df-iin | |- |^|_ x e. A B = { z | A. x e. A z e. B } |
|
| 4 | 2 | nfcri | |- F/ y z e. B |
| 5 | 1 4 | nfralw | |- F/ y A. x e. A z e. B |
| 6 | 5 | nfab | |- F/_ y { z | A. x e. A z e. B } |
| 7 | 3 6 | nfcxfr | |- F/_ y |^|_ x e. A B |