Theorem nfiu1 4550

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 4522	. 2 |- U_ x e. A B = { y | E. x e. A y e. B }
2		nfre1 3005	. . 3 |- F/ x E. x e. A y e. B
3	2	nfab 2769	. 2 |- F/_ x { y | E. x e. A y e. B }
4	1, 3	nfcxfr 2762	1 |- F/_ x U_ x e. A B

Syntax hints:   e. wcel 1990   {cab 2608   F/_wnfc 2751   E.wrex 2913   U_ciun 4520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-iun 4522

This theorem is referenced by:  ssiun2s  4564  disjxiun  4649  disjxiunOLD  4650  triun  4766  iunopeqop  4981  eliunxp  5259  opeliunxp2  5260  opeliunxp2f  7336  ixpf  7930  ixpiunwdom  8496  r1val1  8649  rankuni2b  8716  rankval4  8730  cplem2  8753  ac6num  9301  iunfo  9361  iundom2g  9362  inar1  9597  tskuni  9605  gsum2d2lem  18372  gsum2d2  18373  gsumcom2  18374  iunconn  21231  ptclsg  21418  cnextfvval  21869  ssiun2sf  29378  aciunf1lem  29462  fsumiunle  29575  esum2dlem  30154  esum2d  30155  esumiun  30156  sigapildsys  30225  bnj958  31010  bnj1000  31011  bnj981  31020  bnj1398  31102  bnj1408  31104  iunconnlem2  39171  iunmapss  39407  iunmapsn  39409  allbutfi  39616  fsumiunss  39807  dvnprodlem1  40161  dvnprodlem2  40162  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0iunmpt  40635  iundjiun  40677  voliunsge0lem  40689  caratheodorylem2  40741  smflimmpt  41016  smflimsuplem7  41032  eliunxp2  42112