Theorem nfuni 4872

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

Syntax hints:  Ⅎwnfc 2884  ∪ cuni 4865

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 4866

This theorem is referenced by:  nfiota1  6458  nffrecs  8235  nfsup  9366  ptunimpt  23551  disjabrex  32668  disjabrexf  32669  fnpreimac  32759  nfesum1  34217  nfesum2  34218  bnj1398  35209  bnj1446  35220  bnj1447  35221  bnj1448  35222  bnj1466  35228  bnj1467  35229  bnj1519  35240  bnj1520  35241  bnj1525  35244  bnj1523  35246  dfon2lem3  35996  mptsnunlem  37590  ptrest  37867  heibor1  38058  nfunidALT2  39342  nfunidALT  39343  disjinfi  45548  stoweidlem28  46383  stoweidlem59  46414  fourierdlem80  46541  saliinclf  46681  smfresal  47143  smfpimbor1lem2  47154  nfafv2  47575  nfsetrecs  50042