Theorem nfuni 4880

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

Syntax hints:  Ⅎwnfc 2916  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-uni 4874

This theorem is referenced by:  nfiota1  6491  nffrecs  8276  nfsup  9407  ptunimpt  23717  disjabrex  32864  disjabrexf  32865  fnpreimac  32952  nfesum1  34371  nfesum2  34372  bnj1398  35363  bnj1446  35374  bnj1447  35375  bnj1448  35376  bnj1466  35382  bnj1467  35383  bnj1519  35394  bnj1520  35395  bnj1525  35398  bnj1523  35400  dfon2lem3  36170  mptsnunlem  37867  ptrest  38153  heibor1  38344  nfunidALT2  39628  nfunidALT  39629  disjinfi  45795  stoweidlem28  46627  stoweidlem59  46658  fourierdlem80  46785  saliinclf  46925  smfresal  47387  smfpimbor1lem2  47398  nfafv2  47837  nfsetrecs  50342