Theorem nfuni 4857

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

Syntax hints:  Ⅎwnfc 2883  ∪ cuni 4850

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-uni 4851

This theorem is referenced by:  nfiota1  6456  nffrecs  8233  nfsup  9364  ptunimpt  23560  disjabrex  32652  disjabrexf  32653  fnpreimac  32743  nfesum1  34184  nfesum2  34185  bnj1398  35176  bnj1446  35187  bnj1447  35188  bnj1448  35189  bnj1466  35195  bnj1467  35196  bnj1519  35207  bnj1520  35208  bnj1525  35211  bnj1523  35213  dfon2lem3  35965  mptsnunlem  37654  ptrest  37940  heibor1  38131  nfunidALT2  39415  nfunidALT  39416  disjinfi  45622  stoweidlem28  46456  stoweidlem59  46487  fourierdlem80  46614  saliinclf  46754  smfresal  47216  smfpimbor1lem2  47227  nfafv2  47666  nfsetrecs  50161