Theorem nfuni 4918

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

Syntax hints:  Ⅎwnfc 2887  ∪ cuni 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-uni 4912

This theorem is referenced by:  nfiota1  6517  nffrecs  8306  nfwrecsOLD  8340  nfsup  9488  ptunimpt  23618  disjabrex  32601  disjabrexf  32602  fnpreimac  32687  nfesum1  34020  nfesum2  34021  bnj1398  35026  bnj1446  35037  bnj1447  35038  bnj1448  35039  bnj1466  35045  bnj1467  35046  bnj1519  35057  bnj1520  35058  bnj1525  35061  bnj1523  35063  dfon2lem3  35766  mptsnunlem  37320  ptrest  37605  heibor1  37796  nfunidALT2  38950  nfunidALT  38951  disjinfi  45134  stoweidlem28  45983  stoweidlem59  46014  fourierdlem80  46141  saliinclf  46281  smfresal  46743  smfpimbor1lem2  46754  nfafv2  47167  nfsetrecs  48916