Theorem nfiu1 4355

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)

Assertion

Ref	Expression
nfiu1	|- F/_ x U_ x e. A B

Proof of Theorem nfiu1

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iun 4327	. 2 |- U_ x e. A B = { y | E. x e. A y e. B }
2		nfre1 2925	. . 3 |- F/ x E. x e. A y e. B
3	2	nfab 2633	. 2 |- F/_ x { y | E. x e. A y e. B }
4	1, 3	nfcxfr 2627	1 |- F/_ x U_ x e. A B

Syntax hints:   e. wcel 1767   {cab 2452   F/_wnfc 2615   E.wrex 2815   U_ciun 4325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-iun 4327

This theorem is referenced by:  ssiun2s  4369  disjxiun  4444  triun  4553  eliunxp  5140  opeliunxp2  5141  ixpf  7491  ixpiunwdom  8017  r1val1  8204  rankuni2b  8271  rankval4  8285  cplem2  8308  ac6num  8859  iunfo  8914  iundom2g  8915  inar1  9153  tskuni  9161  gsum2d2lem  16804  gsum2d2  16805  gsumcom2  16806  iuncon  19723  ptclsg  19879  cnextfvval  20328  ssiun2sf  27128  eliunxp2  32019  iunconlem2  32833  bnj958  33095  bnj1000  33096  bnj981  33105  bnj1398  33187  bnj1408  33189