Theorem nfun 4124

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 2179, ax-11 2195, ax-12 2216. (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 4107	. . 3 ⊢ (𝑦 ∈ (𝐴 ∪ 𝐵) ↔ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵))
2		nfun.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2919	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfun.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2919	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfor 1937	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)
7	1, 6	nfxfr 1886	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ (𝐴 ∪ 𝐵)
8	7	nfci 2915	1 ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)

This proof depends on syntax axioms:   ∨ wo 861   ∈ wcel 2146  Ⅎwnfc 2912   ∪ cun 3904

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-v 3459  df-un 3911

This theorem is used by:  nfsymdif  4210  csbun  4406  iunxdif3  5063  nfsuc  6439  nfsup  9418  nfdju  9909  iunconn  23635  nosupbnd2  27931  noinfbnd2  27946  ordtconnlem1  34378  esumsplit  34507  measvuni  34669  bnj958  35393  bnj1000  35394  bnj1408  35489  bnj1446  35498  bnj1447  35499  bnj1448  35500  bnj1466  35506  bnj1467  35507  rdgssun  38081  exrecfnlem  38082  poimirlem16  38344  poimirlem19  38347  pimxrneun  46260  pimrecltpos  47480