Theorem nfun 4072

Description: Bound-variable hypothesis builder for the union of classes. (Contributed by NM, 15-Sep-2003.) (Revised by Mario Carneiro, 14-Oct-2016.)

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		df-un 3865	. 2 ⊢ (𝐴 ∪ 𝐵) = {𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)}
2		nfun.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2906	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfun.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfcri 2906	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐵
6	3, 5	nfor 1905	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)
7	6	nfab 2925	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ (𝑦 ∈ 𝐴 ∨ 𝑦 ∈ 𝐵)}
8	1, 7	nfcxfr 2917	1 ⊢ Ⅎ𝑥(𝐴 ∪ 𝐵)

Syntax hints:   ∨ wo 844   ∈ wcel 2111  {cab 2735  Ⅎwnfc 2899   ∪ cun 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-un 3865

This theorem is referenced by:  nfsymdif  4153  csbun  4338  iunxdif3  4986  nfsuc  6245  nfsup  8961  nfdju  9382  iunconn  22141  ordtconnlem1  31407  esumsplit  31552  measvuni  31713  bnj958  32452  bnj1000  32453  bnj1408  32548  bnj1446  32557  bnj1447  32558  bnj1448  32559  bnj1466  32565  bnj1467  32566  nosupbnd2  33516  noinfbnd2  33531  rdgssun  35109  exrecfnlem  35110  poimirlem16  35387  poimirlem19  35390  pimrecltpos  43745