Theorem nfiu1 4335

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 4307	. 2 |- U_ x e. A B = { y | E. x e. A y e. B }
2		nfre1 2888	. . 3 |- F/ x E. x e. A y e. B
3	2	nfab 2589	. 2 |- F/_ x { y | E. x e. A y e. B }
4	1, 3	nfcxfr 2583	1 |- F/_ x U_ x e. A B

Syntax hints:   e. wcel 1873   {cab 2408   F/_wnfc 2571   E.wrex 2777   U_ciun 4305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rex 2782  df-iun 4307

This theorem is referenced by:  ssiun2s  4349  disjxiun  4426  triun  4537  eliunxp  4997  opeliunxp2  4998  opeliunxp2f  6973  ixpf  7561  ixpiunwdom  8121  r1val1  8271  rankuni2b  8338  rankval4  8352  cplem2  8375  ac6num  8922  iunfo  8977  iundom2g  8978  inar1  9213  tskuni  9221  gsum2d2lem  17610  gsum2d2  17611  gsumcom2  17612  iuncon  20447  ptclsg  20634  cnextfvval  21084  ssiun2sf  28182  aciunf1lem  28272  esum2dlem  28927  esum2d  28928  esumiun  28929  sigapildsys  28998  bnj958  29765  bnj1000  29766  bnj981  29775  bnj1398  29857  bnj1408  29859  iunconlem2  37311  fsumiunss  37601  dvnprodlem1  37767  dvnprodlem2  37768  sge0iunmptlemfi  38169  sge0iunmptlemre  38171  sge0iunmpt  38174  iundjiun  38212  caratheodorylem2  38262  iunopeqop  38876  eliunxp2  39734