Theorem nfun 4132

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 2182, ax-11 2198, ax-12 2219. (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 4115	. . 3 ⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))
2		nfun.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2923	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfun.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2923	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfor 1931	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1880	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∪ 𝐵)
8	7	nfci 2919	1 ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 860   ∈ wcel 2149  Ⅎwnfc 2916   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-v 3465  df-un 3918

This theorem is referenced by:  nfsymdif  4218  csbun  4412  iunxdif3  5065  nfsuc  6436  nfsup  9410  nfdju  9892  iunconn  23553  nosupbnd2  27845  noinfbnd2  27860  ordtconnlem1  34258  esumsplit  34387  measvuni  34548  bnj958  35272  bnj1000  35273  bnj1408  35368  bnj1446  35377  bnj1447  35378  bnj1448  35379  bnj1466  35385  bnj1467  35386  rdgssun  37911  exrecfnlem  37912  poimirlem16  38174  poimirlem19  38177  pimxrneun  46093  pimrecltpos  47313