Theorem nfuni 4879

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

This proof depends on syntax axioms:  Ⅎwnfc 2911  ∪ cuni 4872

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-uni 4873

This theorem is used by:  nfiota1  6522  nffrecs  8339  nfsup  9480  ptunimpt  23969  disjabrex  33274  disjabrexf  33275  fnpreimac  33362  nfesum1  34783  nfesum2  34784  bnj1398  35775  bnj1446  35786  bnj1447  35787  bnj1448  35788  bnj1466  35794  bnj1467  35795  bnj1519  35806  bnj1520  35807  bnj1525  35810  bnj1523  35812  dfon2lem3  36762  mptsnunlem  38529  ptrest  38805  heibor1  39010  nfunidALT2  40292  nfunidALT  40293  disjinfi  46480  stoweidlem28  47311  stoweidlem59  47342  fourierdlem80  47469  saliinclf  47609  smfresal  48071  smfpimbor1lem2  48082  nfafv2  48561  nfsetrecs  51195