Theorem nfun 4117

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 2178, ax-11 2194, ax-12 2213. (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 4100	. . 3 ⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))
2		nfun.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2914	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfun.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2914	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfor 1937	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1886	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∪ 𝐵)
8	7	nfci 2910	1 ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)

This proof depends on syntax axioms:   ∨ wo 861   ∈ wcel 2145  Ⅎwnfc 2907   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-v 3452  df-un 3904

This theorem is used by:  nfsymdif  4203  csbun  4399  iunxdif3  5055  nfsuc  6432  nfsup  9421  nfdju  9912  iunconn  23653  nosupbnd2  27952  noinfbnd2  27967  ordtconnlem1  34434  esumsplit  34563  measvuni  34725  bnj958  35449  bnj1000  35450  bnj1408  35545  bnj1446  35554  bnj1447  35555  bnj1448  35556  bnj1466  35562  bnj1467  35563  rdgssun  38132  exrecfnlem  38133  poimirlem16  38385  poimirlem19  38388  pimxrneun  46316  pimrecltpos  47536