Description: Bound-variable hypothesis builder for indexed union. Usage of this theorem is discouraged because it depends on ax-13 , see nfiund for a weaker version that does not require it. (Contributed by Emmett Weisz, 6-Dec-2019) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nfiundg.1 | |- F/ x ph |
|
nfiundg.2 | |- ( ph -> F/_ y A ) |
||
nfiundg.3 | |- ( ph -> F/_ y B ) |
||
Assertion | nfiundg | |- ( ph -> F/_ y U_ x e. A B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfiundg.1 | |- F/ x ph |
|
2 | nfiundg.2 | |- ( ph -> F/_ y A ) |
|
3 | nfiundg.3 | |- ( ph -> F/_ y B ) |
|
4 | df-iun | |- U_ x e. A B = { z | E. x e. A z e. B } |
|
5 | nfv | |- F/ z ph |
|
6 | 3 | nfcrd | |- ( ph -> F/ y z e. B ) |
7 | 1 2 6 | nfrexdg | |- ( ph -> F/ y E. x e. A z e. B ) |
8 | 5 7 | nfabd | |- ( ph -> F/_ y { z | E. x e. A z e. B } ) |
9 | 4 8 | nfcxfrd | |- ( ph -> F/_ y U_ x e. A B ) |