Metamath Proof Explorer


Theorem nfiundg

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 )

Proof

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 )