Theorem nfuni 4881

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

This proof depends on syntax axioms:  Ⅎwnfc 2912  ∪ cuni 4874

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-uni 4875

This theorem is used by:  nfiota1  6498  nffrecs  8282  nfsup  9414  ptunimpt  23781  disjabrex  32956  disjabrexf  32957  fnpreimac  33044  nfesum1  34453  nfesum2  34454  bnj1398  35446  bnj1446  35457  bnj1447  35458  bnj1448  35459  bnj1466  35465  bnj1467  35466  bnj1519  35477  bnj1520  35478  bnj1525  35481  bnj1523  35483  dfon2lem3  36288  mptsnunlem  38017  ptrest  38303  heibor1  38494  nfunidALT2  39776  nfunidALT  39777  disjinfi  45943  stoweidlem28  46775  stoweidlem59  46806  fourierdlem80  46933  saliinclf  47073  smfresal  47535  smfpimbor1lem2  47546  nfafv2  47988  nfsetrecs  50497