Theorem nfuni 4870

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

Syntax hints:  Ⅎwnfc 2883  ∪ cuni 4863

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

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

This theorem is referenced by:  nfiota1  6450  nffrecs  8225  nfsup  9354  ptunimpt  23539  disjabrex  32657  disjabrexf  32658  fnpreimac  32749  nfesum1  34197  nfesum2  34198  bnj1398  35190  bnj1446  35201  bnj1447  35202  bnj1448  35203  bnj1466  35209  bnj1467  35210  bnj1519  35221  bnj1520  35222  bnj1525  35225  bnj1523  35227  dfon2lem3  35977  mptsnunlem  37543  ptrest  37820  heibor1  38011  nfunidALT2  39229  nfunidALT  39230  disjinfi  45436  stoweidlem28  46272  stoweidlem59  46303  fourierdlem80  46430  saliinclf  46570  smfresal  47032  smfpimbor1lem2  47043  nfafv2  47464  nfsetrecs  49931