Theorem nfuni 4712

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

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfuni2 4708	. 2 ⊢ ∪ 𝐴 = {𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 ∈ 𝑧}
2		nfuni.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1873	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝑧
4	2, 3	nfrex 3247	. . 3 ⊢ Ⅎ𝑥∃𝑧 ∈ 𝐴 𝑦 ∈ 𝑧
5	4	nfab 2932	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑧 ∈ 𝐴 𝑦 ∈ 𝑧}
6	1, 5	nfcxfr 2924	1 ⊢ Ⅎ𝑥∪ 𝐴

Syntax hints:  {cab 2753  Ⅎwnfc 2910  ∃wrex 3083  ∪ cuni 4706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-uni 4707

This theorem is referenced by:  nfiota1  6148  nfwrecs  7745  nfsup  8702  ptunimpt  21897  disjabrex  30088  disjabrexf  30089  fnpreimac  30168  nfesum1  30900  nfesum2  30901  bnj1398  31912  bnj1446  31923  bnj1447  31924  bnj1448  31925  bnj1466  31931  bnj1467  31932  bnj1519  31943  bnj1520  31944  bnj1525  31947  bnj1523  31949  dfon2lem3  32490  nffrecs  32581  mptsnunlem  33996  ptrest  34280  heibor1  34478  nfunidALT2  35498  nfunidALT  35499  disjinfi  40824  stoweidlem28  41690  stoweidlem59  41721  fourierdlem80  41848  smfresal  42440  smfpimbor1lem2  42451  nfafv2  42769  nfsetrecs  44096