Theorem nfuni 4442

Description: Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Hypothesis

Ref	Expression
nfuni.1	|- F/_ x A

Assertion

Ref	Expression
nfuni	|- F/_ x U. A

Proof of Theorem nfuni

Dummy variables y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfuni2 4438	. 2 |- U. A = { y | E. z e. A y e. z }
2		nfuni.1	. . . 4 |- F/_ x A
3		nfv 1843	. . . 4 |- F/ x y e. z
4	2, 3	nfrex 3007	. . 3 |- F/ x E. z e. A y e. z
5	4	nfab 2769	. 2 |- F/_ x { y | E. z e. A y e. z }
6	1, 5	nfcxfr 2762	1 |- F/_ x U. A

Syntax hints:   {cab 2608   F/_wnfc 2751   E.wrex 2913   U.cuni 4436

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-ral 2917  df-rex 2918  df-uni 4437

This theorem is referenced by:  nfiota1  5853  nfwrecs  7409  nfsup  8357  ptunimpt  21398  disjabrex  29395  disjabrexf  29396  nfesum1  30102  nfesum2  30103  bnj1398  31102  bnj1446  31113  bnj1447  31114  bnj1448  31115  bnj1466  31121  bnj1467  31122  bnj1519  31133  bnj1520  31134  bnj1525  31137  bnj1523  31139  dfon2lem3  31690  mptsnunlem  33185  ptrest  33408  heibor1  33609  nfunidALT2  34256  nfunidALT  34257  disjinfi  39380  stoweidlem28  40245  stoweidlem59  40276  fourierdlem80  40403  smfresal  40995  smfpimbor1lem2  41006  nfsetrecs  42433