Theorem nfuni 4872

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

Syntax hints:  Ⅎwnfc 2884  ∪ cuni 4865

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-uni 4866

This theorem is referenced by:  nfiota1  6460  nffrecs  8237  nfsup  9368  ptunimpt  23556  disjabrex  32675  disjabrexf  32676  fnpreimac  32766  nfesum1  34224  nfesum2  34225  bnj1398  35216  bnj1446  35227  bnj1447  35228  bnj1448  35229  bnj1466  35235  bnj1467  35236  bnj1519  35247  bnj1520  35248  bnj1525  35251  bnj1523  35253  dfon2lem3  36005  mptsnunlem  37620  ptrest  37899  heibor1  38090  nfunidALT2  39374  nfunidALT  39375  disjinfi  45580  stoweidlem28  46415  stoweidlem59  46446  fourierdlem80  46573  saliinclf  46713  smfresal  47175  smfpimbor1lem2  47186  nfafv2  47607  nfsetrecs  50074