Theorem nfuni 4920

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

Syntax hints:  Ⅎwnfc 2876  ∪ cuni 4913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-uni 4914

This theorem is referenced by:  nfiota1  6508  nffrecs  8298  nfwrecsOLD  8332  nfsup  9494  ptunimpt  23590  disjabrex  32502  disjabrexf  32503  fnpreimac  32588  nfesum1  33873  nfesum2  33874  bnj1398  34879  bnj1446  34890  bnj1447  34891  bnj1448  34892  bnj1466  34898  bnj1467  34899  bnj1519  34910  bnj1520  34911  bnj1525  34914  bnj1523  34916  dfon2lem3  35609  mptsnunlem  37045  ptrest  37320  heibor1  37511  nfunidALT2  38667  nfunidALT  38668  disjinfi  44799  stoweidlem28  45649  stoweidlem59  45680  fourierdlem80  45807  saliinclf  45947  smfresal  46409  smfpimbor1lem2  46420  nfafv2  46831  nfsetrecs  48432