Theorem nfun 4193

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 2158, ax-12 2178. (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 4176	. . 3 ⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))
2		nfun.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2900	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfun.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2900	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfor 1903	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1851	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∪ 𝐵)
8	7	nfci 2896	1 ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 846   ∈ wcel 2108  Ⅎwnfc 2893   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-v 3490  df-un 3981

This theorem is referenced by:  nfsymdif  4276  csbun  4464  iunxdif3  5118  nfsuc  6467  nfsup  9520  nfdju  9976  iunconn  23457  nosupbnd2  27779  noinfbnd2  27794  ordtconnlem1  33870  esumsplit  34017  measvuni  34178  bnj958  34916  bnj1000  34917  bnj1408  35012  bnj1446  35021  bnj1447  35022  bnj1448  35023  bnj1466  35029  bnj1467  35030  rdgssun  37344  exrecfnlem  37345  poimirlem16  37596  poimirlem19  37599  pimxrneun  45404  pimrecltpos  46629