Theorem nfiun 5004

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 5006 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 4974	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
2		nfiun.1	. . . 4 ⊢ Ⅎ𝑦𝐴
3		nfiun.2	. . . . 5 ⊢ Ⅎ𝑦𝐵
4	3	nfcri 2891	. . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
5	2, 4	nfrexw 3297	. . 3 ⊢ Ⅎ𝑦∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵
6	5	nfab 2905	. 2 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
7	1, 6	nfcxfr 2897	1 ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2109  {cab 2714  Ⅎwnfc 2884  ∃wrex 3061  ∪ ciun 4972

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-iun 4974

This theorem is referenced by:  iunab  5032  disjxiun  5121  ttrclselem1  9744  ttrclselem2  9745  ovoliunnul  25465  iunxpssiun1  32554  iundisjf  32575  iundisj2f  32576  iundisjfi  32778  iundisj2fi  32779  bnj1498  35097  ss2iundf  43658  nfcoll  44255  fnlimcnv  45676  fnlimfvre  45683  fnlimabslt  45688  smfaddlem1  46772  smflimlem6  46785  smflim  46786  smfmullem4  46803  smflim2  46815  smflimsup  46837  smfliminf  46840  fsupdm  46851  finfdm  46855