Theorem nfuni 4867

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

Syntax hints:  Ⅎwnfc 2880  ∪ cuni 4860

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 2182  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-uni 4861

This theorem is referenced by:  nfiota1  6447  nffrecs  8222  nfsup  9346  ptunimpt  23530  disjabrex  32583  disjabrexf  32584  fnpreimac  32675  nfesum1  34125  nfesum2  34126  bnj1398  35118  bnj1446  35129  bnj1447  35130  bnj1448  35131  bnj1466  35137  bnj1467  35138  bnj1519  35149  bnj1520  35150  bnj1525  35153  bnj1523  35155  dfon2lem3  35899  mptsnunlem  37455  ptrest  37732  heibor1  37923  nfunidALT2  39141  nfunidALT  39142  disjinfi  45352  stoweidlem28  46188  stoweidlem59  46219  fourierdlem80  46346  saliinclf  46486  smfresal  46948  smfpimbor1lem2  46959  nfafv2  47380  nfsetrecs  49847