Theorem nfuni 4869

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

Syntax hints:  Ⅎwnfc 2908  ∪ cuni 4862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-uni 4863

This theorem is referenced by:  nfiota1  6474  nffrecs  8258  nfsup  9391  ptunimpt  23643  disjabrex  32742  disjabrexf  32743  fnpreimac  32833  nfesum1  34298  nfesum2  34299  bnj1398  35290  bnj1446  35301  bnj1447  35302  bnj1448  35303  bnj1466  35309  bnj1467  35310  bnj1519  35321  bnj1520  35322  bnj1525  35325  bnj1523  35327  dfon2lem3  36094  mptsnunlem  37793  ptrest  38079  heibor1  38270  nfunidALT2  39554  nfunidALT  39555  disjinfi  45731  stoweidlem28  46563  stoweidlem59  46594  fourierdlem80  46721  saliinclf  46861  smfresal  47323  smfpimbor1lem2  47334  nfafv2  47773  nfsetrecs  50268