Theorem nfiun 4980

Description: Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2377. See nfiung 4982 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)

Hypotheses

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

Assertion

Ref	Expression
nfiun	⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem nfiun

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iun 4950	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
2		nfiun.1	. . . 4 ⊢ Ⅎ𝑦𝐴
3		nfiun.2	. . . . 5 ⊢ Ⅎ𝑦𝐵
4	3	nfcri 2891	. . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
5	2, 4	nfrexw 3286	. . 3 ⊢ Ⅎ𝑦∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵
6	5	nfab 2905	. 2 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
7	1, 6	nfcxfr 2897	1 ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2114  {cab 2715  Ⅎwnfc 2884  ∃wrex 3062  ∪ ciun 4948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-iun 4950

This theorem is referenced by:  iunab  5009  disjxiun  5097  ttrclselem1  9646  ttrclselem2  9647  ovoliunnul  25479  iunxpssiun1  32659  iundisjf  32680  iundisj2f  32681  iundisjfi  32891  iundisj2fi  32892  suppgsumssiun  33170  bnj1498  35241  ss2iundf  44019  nfcoll  44616  fnlimcnv  46029  fnlimfvre  46036  fnlimabslt  46041  smfaddlem1  47125  smflimlem6  47138  smflim  47139  smfmullem4  47156  smflim2  47168  smflimsup  47190  smfliminf  47193  fsupdm  47204  finfdm  47208