Theorem nfuni 4852

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

Syntax hints:  Ⅎwnfc 2887  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-uni 4846

This theorem is referenced by:  nfiota1  6450  nffrecs  8230  nfsup  9361  ptunimpt  23585  disjabrex  32678  disjabrexf  32679  fnpreimac  32769  nfesum1  34231  nfesum2  34232  bnj1398  35223  bnj1446  35234  bnj1447  35235  bnj1448  35236  bnj1466  35242  bnj1467  35243  bnj1519  35254  bnj1520  35255  bnj1525  35258  bnj1523  35260  dfon2lem3  36018  mptsnunlem  37707  ptrest  37993  heibor1  38184  nfunidALT2  39468  nfunidALT  39469  disjinfi  45646  stoweidlem28  46478  stoweidlem59  46509  fourierdlem80  46636  saliinclf  46776  smfresal  47238  smfpimbor1lem2  47249  nfafv2  47688  nfsetrecs  50183