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 2908  ∪ 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 2733

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 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-uni 4868

This theorem is used by:  nfiota1  6495  nffrecs  8294  nfsup  9436  ptunimpt  23907  disjabrex  33169  disjabrexf  33170  fnpreimac  33257  nfesum1  34665  nfesum2  34666  bnj1398  35657  bnj1446  35668  bnj1447  35669  bnj1448  35670  bnj1466  35676  bnj1467  35677  bnj1519  35688  bnj1520  35689  bnj1525  35692  bnj1523  35694  dfon2lem3  36527  mptsnunlem  38241  ptrest  38517  heibor1  38724  nfunidALT2  40006  nfunidALT  40007  disjinfi  46176  stoweidlem28  47007  stoweidlem59  47038  fourierdlem80  47165  saliinclf  47305  smfresal  47767  smfpimbor1lem2  47778  nfafv2  48257  nfsetrecs  50758