Theorem nfuni 4890

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

Syntax hints:  Ⅎwnfc 2883  ∪ cuni 4883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-uni 4884

This theorem is referenced by:  nfiota1  6486  nffrecs  8282  nfwrecsOLD  8316  nfsup  9463  ptunimpt  23533  disjabrex  32563  disjabrexf  32564  fnpreimac  32649  nfesum1  34071  nfesum2  34072  bnj1398  35065  bnj1446  35076  bnj1447  35077  bnj1448  35078  bnj1466  35084  bnj1467  35085  bnj1519  35096  bnj1520  35097  bnj1525  35100  bnj1523  35102  dfon2lem3  35803  mptsnunlem  37356  ptrest  37643  heibor1  37834  nfunidALT2  38987  nfunidALT  38988  disjinfi  45216  stoweidlem28  46057  stoweidlem59  46088  fourierdlem80  46215  saliinclf  46355  smfresal  46817  smfpimbor1lem2  46828  nfafv2  47247  nfsetrecs  49550