Description: Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014) Add disjoint variable condition to avoid ax-13 . See nfiung 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 | nfiun | |- F/_ y U_ x e. A B |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfiun.1 | |- F/_ y A |
|
| 2 | nfiun.2 | |- F/_ y B |
|
| 3 | df-iun | |- U_ x e. A B = { z | E. x e. A z e. B } |
|
| 4 | 2 | nfcri | |- F/ y z e. B |
| 5 | 1 4 | nfrexw | |- F/ y E. x e. A z e. B |
| 6 | 5 | nfab | |- F/_ y { z | E. x e. A z e. B } |
| 7 | 3 6 | nfcxfr | |- F/_ y U_ x e. A B |