Theorem nfuni 4858

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	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfuni	⊢ Ⅎ𝑥∪ 𝐴

Proof of Theorem nfuni

Step	Hyp	Ref	Expression
1		nfuni.1	. 2 ⊢ Ⅎ𝑥𝐴
2		id 22	. . 3 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥𝐴)
3	2	nfunid 4857	. 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥∪ 𝐴)
4	1, 3	ax-mp 5	1 ⊢ Ⅎ𝑥∪ 𝐴

Syntax hints:  Ⅎwnfc 2884  ∪ cuni 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-uni 4852

This theorem is referenced by:  nfiota1  6450  nffrecs  8226  nfsup  9357  ptunimpt  23570  disjabrex  32667  disjabrexf  32668  fnpreimac  32758  nfesum1  34200  nfesum2  34201  bnj1398  35192  bnj1446  35203  bnj1447  35204  bnj1448  35205  bnj1466  35211  bnj1467  35212  bnj1519  35223  bnj1520  35224  bnj1525  35227  bnj1523  35229  dfon2lem3  35981  mptsnunlem  37668  ptrest  37954  heibor1  38145  nfunidALT2  39429  nfunidALT  39430  disjinfi  45640  stoweidlem28  46474  stoweidlem59  46505  fourierdlem80  46632  saliinclf  46772  smfresal  47234  smfpimbor1lem2  47245  nfafv2  47678  nfsetrecs  50173