Theorem nfun 4145

Description: Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.) Avoid ax-10 2141, ax-11 2157, ax-12 2177. (Revised by SN, 14-May-2025.)

Hypotheses

Ref	Expression
nfun.1	⊢ Ⅎ𝑥𝐴
nfun.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfun	⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)

Proof of Theorem nfun

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elun 4128	. . 3 ⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))
2		nfun.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2890	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfun.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2890	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfor 1904	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1853	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∪ 𝐵)
8	7	nfci 2886	1 ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 847   ∈ wcel 2108  Ⅎwnfc 2883   ∪ cun 3924

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-v 3461  df-un 3931

This theorem is referenced by:  nfsymdif  4232  csbun  4416  iunxdif3  5071  nfsuc  6426  nfsup  9463  nfdju  9921  iunconn  23366  nosupbnd2  27680  noinfbnd2  27695  ordtconnlem1  33955  esumsplit  34084  measvuni  34245  bnj958  34971  bnj1000  34972  bnj1408  35067  bnj1446  35076  bnj1447  35077  bnj1448  35078  bnj1466  35084  bnj1467  35085  rdgssun  37396  exrecfnlem  37397  poimirlem16  37660  poimirlem19  37663  pimxrneun  45515  pimrecltpos  46737