Theorem nfuni 4851

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

Syntax hints:  Ⅎwnfc 2885  ∪ cuni 4844

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ral 3063  df-rex 3072  df-uni 4845

This theorem is referenced by:  nfiota1  6412  nffrecs  8130  nfwrecsOLD  8164  nfsup  9258  ptunimpt  22795  disjabrex  30970  disjabrexf  30971  fnpreimac  31057  nfesum1  32057  nfesum2  32058  bnj1398  33063  bnj1446  33074  bnj1447  33075  bnj1448  33076  bnj1466  33082  bnj1467  33083  bnj1519  33094  bnj1520  33095  bnj1525  33098  bnj1523  33100  dfon2lem3  33810  mptsnunlem  35557  ptrest  35824  heibor1  36016  nfunidALT2  37183  nfunidALT  37184  disjinfi  42951  stoweidlem28  43798  stoweidlem59  43829  fourierdlem80  43956  smfresal  44556  smfpimbor1lem2  44567  nfafv2  44954  nfsetrecs  46636