Theorem nfuni 4938

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

Syntax hints:  Ⅎwnfc 2893  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-uni 4932

This theorem is referenced by:  nfiota1  6527  nffrecs  8324  nfwrecsOLD  8358  nfsup  9520  ptunimpt  23624  disjabrex  32604  disjabrexf  32605  fnpreimac  32689  nfesum1  34004  nfesum2  34005  bnj1398  35010  bnj1446  35021  bnj1447  35022  bnj1448  35023  bnj1466  35029  bnj1467  35030  bnj1519  35041  bnj1520  35042  bnj1525  35045  bnj1523  35047  dfon2lem3  35749  mptsnunlem  37304  ptrest  37579  heibor1  37770  nfunidALT2  38925  nfunidALT  38926  disjinfi  45099  stoweidlem28  45949  stoweidlem59  45980  fourierdlem80  46107  saliinclf  46247  smfresal  46709  smfpimbor1lem2  46720  nfafv2  47133  nfsetrecs  48778