Theorem nfuni 4878

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

Syntax hints:  Ⅎwnfc 2876  ∪ cuni 4871

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-uni 4872

This theorem is referenced by:  nfiota1  6466  nffrecs  8262  nfsup  9402  ptunimpt  23482  disjabrex  32511  disjabrexf  32512  fnpreimac  32595  nfesum1  34030  nfesum2  34031  bnj1398  35024  bnj1446  35035  bnj1447  35036  bnj1448  35037  bnj1466  35043  bnj1467  35044  bnj1519  35055  bnj1520  35056  bnj1525  35059  bnj1523  35061  dfon2lem3  35773  mptsnunlem  37326  ptrest  37613  heibor1  37804  nfunidALT2  38962  nfunidALT  38963  disjinfi  45186  stoweidlem28  46026  stoweidlem59  46057  fourierdlem80  46184  saliinclf  46324  smfresal  46786  smfpimbor1lem2  46797  nfafv2  47219  nfsetrecs  49675