Theorem nfuni 4874

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

This proof depends on syntax axioms:  Ⅎwnfc 2907  ∪ cuni 4867

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-uni 4868

This theorem is used by:  nfiota1  6491  nffrecs  8282  nfsup  9421  ptunimpt  23821  disjabrex  33055  disjabrexf  33056  fnpreimac  33143  nfesum1  34550  nfesum2  34551  bnj1398  35543  bnj1446  35554  bnj1447  35555  bnj1448  35556  bnj1466  35562  bnj1467  35563  bnj1519  35574  bnj1520  35575  bnj1525  35578  bnj1523  35580  dfon2lem3  36362  mptsnunlem  38092  ptrest  38368  heibor1  38560  nfunidALT2  39842  nfunidALT  39843  disjinfi  46024  stoweidlem28  46856  stoweidlem59  46887  fourierdlem80  47014  saliinclf  47154  smfresal  47616  smfpimbor1lem2  47627  nfafv2  48106  nfsetrecs  50612