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 2915	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfun.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2915	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfor 1937	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1886	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∪ 𝐵)
8	7	nfci 2911	1 ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)

This proof depends on syntax axioms:   ∨ wo 861   ∈ wcel 2145  Ⅎwnfc 2908   ∪ 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 2733

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 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-v 3453  df-un 3904

This theorem is used by:  nfsymdif  4203  csbun  4399  iunxdif3  5055  nfsuc  6436  nfsup  9436  nfdju  9981  iunconn  23739  nosupbnd2  28066  noinfbnd2  28081  ordtconnlem1  34549  esumsplit  34678  measvuni  34840  bnj958  35563  bnj1000  35564  bnj1408  35659  bnj1446  35668  bnj1447  35669  bnj1448  35670  bnj1466  35676  bnj1467  35677  rdgssun  38281  exrecfnlem  38282  poimirlem16  38534  poimirlem19  38537  pimxrneun  46467  pimrecltpos  47687