Theorem nfiun 4988

Description: Bound-variable hypothesis builder for indexed union. (Contributed by Mario Carneiro, 25-Jan-2014.) Add disjoint variable condition to avoid ax-13 2404. See nfiung 4990 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 4958	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
2		nfiun.1	. . . 4 ⊢ Ⅎ𝑦𝐴
3		nfiun.2	. . . . 5 ⊢ Ⅎ𝑦𝐵
4	3	nfcri 2917	. . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵
5	2, 4	nfrexw 3313	. . 3 ⊢ Ⅎ𝑦∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵
6	5	nfab 2931	. 2 ⊢ Ⅎ𝑦{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
7	1, 6	nfcxfr 2923	1 ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵

This proof depends on syntax axioms:   ∈ wcel 2143  {cab 2741  Ⅎwnfc 2910  ∃wrex 3089  ∪ ciun 4956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-iun 4958

This theorem is used by:  iunab  5016  disjxiun  5106  ttrclselem1  9690  ttrclselem2  9691  ovoliunnul  25675  iunxpssiun1  32922  iundisjf  32943  iundisj2f  32944  iundisjfi  33150  iundisj2fi  33151  suppgsumssiun  33401  bnj1498  35458  nfttc  37030  ss2iundf  44413  nfcoll  44994  fnlimcnv  46409  fnlimfvre  46416  fnlimabslt  46421  smfaddlem1  47505  smflimlem6  47518  smflim  47519  smfmullem4  47536  smflim2  47548  smflimsup  47570  smfliminf  47573  fsupdm  47584  finfdm  47588