Theorem nfuni 4873

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-uni 4867

This theorem is used by:  nfiota1  6496  nffrecs  8305  nfsup  9447  ptunimpt  23920  disjabrex  33224  disjabrexf  33225  fnpreimac  33312  nfesum1  34719  nfesum2  34720  bnj1398  35711  bnj1446  35722  bnj1447  35723  bnj1448  35724  bnj1466  35730  bnj1467  35731  bnj1519  35742  bnj1520  35743  bnj1525  35746  bnj1523  35748  dfon2lem3  36640  mptsnunlem  38355  ptrest  38631  heibor1  38838  nfunidALT2  40120  nfunidALT  40121  disjinfi  46301  stoweidlem28  47132  stoweidlem59  47163  fourierdlem80  47290  saliinclf  47430  smfresal  47892  smfpimbor1lem2  47903  nfafv2  48382  nfsetrecs  50958