Theorem nfun 4123

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 2175, ax-11 2191, ax-12 2212. (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 4106	. . 3 ⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))
2		nfun.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2916	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfun.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2916	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfor 1924	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1873	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∪ 𝐵)
8	7	nfci 2912	1 ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 858   ∈ wcel 2142  Ⅎwnfc 2909   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-v 3456  df-un 3909

This theorem is referenced by:  nfsymdif  4209  csbun  4395  iunxdif3  5052  nfsuc  6420  nfsup  9397  nfdju  9865  iunconn  23485  nosupbnd2  27777  noinfbnd2  27792  ordtconnlem1  34218  esumsplit  34347  measvuni  34508  bnj958  35232  bnj1000  35233  bnj1408  35328  bnj1446  35337  bnj1447  35338  bnj1448  35339  bnj1466  35345  bnj1467  35346  rdgssun  37869  exrecfnlem  37870  poimirlem16  38132  poimirlem19  38135  pimxrneun  46059  pimrecltpos  47279