Theorem nfuni 4868

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

Syntax hints:  Ⅎwnfc 2876  ∪ cuni 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-uni 4862

This theorem is referenced by:  nfiota1  6444  nffrecs  8223  nfsup  9360  ptunimpt  23498  disjabrex  32544  disjabrexf  32545  fnpreimac  32628  nfesum1  34009  nfesum2  34010  bnj1398  35003  bnj1446  35014  bnj1447  35015  bnj1448  35016  bnj1466  35022  bnj1467  35023  bnj1519  35034  bnj1520  35035  bnj1525  35038  bnj1523  35040  dfon2lem3  35761  mptsnunlem  37314  ptrest  37601  heibor1  37792  nfunidALT2  38950  nfunidALT  38951  disjinfi  45173  stoweidlem28  46013  stoweidlem59  46044  fourierdlem80  46171  saliinclf  46311  smfresal  46773  smfpimbor1lem2  46784  nfafv2  47206  nfsetrecs  49675