Theorem nfiu1 4299

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 4271	. 2 |- U_ x e. A B = { y | E. x e. A y e. B }
2		nfre1 2846	. . 3 |- F/ x E. x e. A y e. B
3	2	nfab 2616	. 2 |- F/_ x { y | E. x e. A y e. B }
4	1, 3	nfcxfr 2610	1 |- F/_ x U_ x e. A B

Syntax hints:   e. wcel 1904   {cab 2457   F/_wnfc 2599   E.wrex 2757   U_ciun 4269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rex 2762  df-iun 4271

This theorem is referenced by:  ssiun2s  4313  disjxiun  4392  triun  4503  eliunxp  4977  opeliunxp2  4978  opeliunxp2f  6975  ixpf  7562  ixpiunwdom  8124  r1val1  8275  rankuni2b  8342  rankval4  8356  cplem2  8379  ac6num  8927  iunfo  8982  iundom2g  8983  inar1  9218  tskuni  9226  gsum2d2lem  17683  gsum2d2  17684  gsumcom2  17685  iuncon  20520  ptclsg  20707  cnextfvval  21158  ssiun2sf  28252  aciunf1lem  28339  esum2dlem  28987  esum2d  28988  esumiun  28989  sigapildsys  29058  bnj958  29823  bnj1000  29824  bnj981  29833  bnj1398  29915  bnj1408  29917  iunconlem2  37395  iunmapss  37568  iunmapsn  37570  fsumiunss  37750  dvnprodlem1  37918  dvnprodlem2  37919  sge0iunmptlemfi  38369  sge0iunmptlemre  38371  sge0iunmpt  38374  iundjiun  38414  voliunsge0lem  38426  caratheodorylem2  38467  iunopeqop  39151  eliunxp2  40623