Theorem nfuni 4861

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 4860	. 2 ⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥∪ 𝐴)
4	1, 3	ax-mp 5	1 ⊢ Ⅎ𝑥∪ 𝐴

Syntax hints:  Ⅎwnfc 2879  ∪ cuni 4854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-uni 4855

This theorem is referenced by:  nfiota1  6434  nffrecs  8208  nfsup  9330  ptunimpt  23505  disjabrex  32554  disjabrexf  32555  fnpreimac  32645  nfesum1  34045  nfesum2  34046  bnj1398  35038  bnj1446  35049  bnj1447  35050  bnj1448  35051  bnj1466  35057  bnj1467  35058  bnj1519  35069  bnj1520  35070  bnj1525  35073  bnj1523  35075  dfon2lem3  35819  mptsnunlem  37372  ptrest  37659  heibor1  37850  nfunidALT2  39008  nfunidALT  39009  disjinfi  45229  stoweidlem28  46066  stoweidlem59  46097  fourierdlem80  46224  saliinclf  46364  smfresal  46826  smfpimbor1lem2  46837  nfafv2  47249  nfsetrecs  49718