Theorem nfiun 4747

Description: Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.)

Hypotheses

Ref	Expression
nfiun.1	⊢ Ⅎ𝑦𝐴
nfiun.2	⊢ Ⅎ𝑦𝐵

Assertion

Ref	Expression
nfiun	⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵

Proof of Theorem nfiun

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iun 4721	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
2		nfiun.1	. . . 4 ⊢ Ⅎ𝑦𝐴
3		nfiun.2	. . . . 5 ⊢ Ⅎ𝑦𝐵
4	3	nfcri 2949	. . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
5	2, 4	nfrex 3201	. . 3 ⊢ Ⅎ𝑦∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵
6	5	nfab 2960	. 2 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
7	1, 6	nfcxfr 2953	1 ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2157  {cab 2799  Ⅎwnfc 2942  ∃wrex 3104  ∪ ciun 4719

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rex 3109  df-iun 4721

This theorem is referenced by:  iunab  4765  disjxiun  4848  ovoliunnul  23494  iundisjf  29733  iundisj2f  29734  iundisjfi  29888  iundisj2fi  29889  bnj1498  31457  trpredlem1  32052  trpredrec  32063  ss2iundf  38452  fnlimcnv  40380  fnlimfvre  40387  fnlimabslt  40392  smfaddlem1  41454  smflimlem6  41467  smflim  41468  smfmullem4  41484  smflim2  41495  smflimsup  41517  smfliminf  41520