Theorem nfuni 4880

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

Syntax hints:  Ⅎwnfc 2910  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-uni 4874

This theorem is referenced by:  nfiota1  6496  nffrecs  8281  nfsup  9412  ptunimpt  23733  disjabrex  32908  disjabrexf  32909  fnpreimac  32996  nfesum1  34411  nfesum2  34412  bnj1398  35403  bnj1446  35414  bnj1447  35415  bnj1448  35416  bnj1466  35422  bnj1467  35423  bnj1519  35434  bnj1520  35435  bnj1525  35438  bnj1523  35440  dfon2lem3  36256  mptsnunlem  37965  ptrest  38251  heibor1  38442  nfunidALT2  39724  nfunidALT  39725  disjinfi  45893  stoweidlem28  46725  stoweidlem59  46756  fourierdlem80  46883  saliinclf  47023  smfresal  47485  smfpimbor1lem2  47496  nfafv2  47938  nfsetrecs  50447