Theorem nfiu1 4332

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

Syntax hints:   e. wcel 1870   {cab 2414   F/_wnfc 2577   E.wrex 2783   U_ciun 4302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rex 2788  df-iun 4304

This theorem is referenced by:  ssiun2s  4346  disjxiun  4423  triun  4533  eliunxp  4992  opeliunxp2  4993  ixpf  7552  ixpiunwdom  8106  r1val1  8256  rankuni2b  8323  rankval4  8337  cplem2  8360  ac6num  8907  iunfo  8962  iundom2g  8963  inar1  9199  tskuni  9207  gsum2d2lem  17540  gsum2d2  17541  gsumcom2  17542  iuncon  20374  ptclsg  20561  cnextfvval  21011  ssiun2sf  28013  aciunf1lem  28104  esum2dlem  28752  esum2d  28753  esumiun  28754  sigapildsys  28823  bnj958  29539  bnj1000  29540  bnj981  29549  bnj1398  29631  bnj1408  29633  iunconlem2  36972  fsumiunss  37229  dvnprodlem1  37390  dvnprodlem2  37391  sge0iunmptlemfi  37789  sge0iunmptlemre  37791  sge0iunmpt  37794  iundjiun  37807  caratheodorylem2  37857  eliunxp2  38875