Theorem nfiu1 4958

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)

Assertion

Ref	Expression
nfiu1	⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Proof of Theorem nfiu1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iun 4926	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfre1 3239	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2913	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2905	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2106  {cab 2715  Ⅎwnfc 2887  ∃wrex 3065  ∪ ciun 4924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-rex 3070  df-iun 4926

This theorem is referenced by:  ssiun2s  4978  disjxiun  5071  triun  5204  iunopeqop  5435  eliunxp  5746  opeliunxp2  5747  opeliunxp2f  8026  ixpf  8708  ixpiunwdom  9349  r1val1  9544  rankuni2b  9611  rankval4  9625  cplem2  9648  ac6num  10235  iunfo  10295  iundom2g  10296  inar1  10531  tskuni  10539  gsum2d2lem  19574  gsum2d2  19575  gsumcom2  19576  iunconn  22579  ptclsg  22766  cnextfvval  23216  ssiun2sf  30899  djussxp2  30985  2ndresdju  30986  aciunf1lem  30999  fsumiunle  31143  esum2dlem  32060  esum2d  32061  esumiun  32062  sigapildsys  32130  bnj958  32920  bnj1000  32921  bnj981  32930  bnj1398  33014  bnj1408  33016  ralssiun  35578  iunconnlem2  42555  iunmapss  42755  iunmapsn  42757  allbutfi  42933  fsumiunss  43116  dvnprodlem1  43487  dvnprodlem2  43488  sge0iunmptlemfi  43951  sge0iunmptlemre  43953  sge0iunmpt  43956  iundjiun  43998  voliunsge0lem  44010  caratheodorylem2  44065  smflimmpt  44343  smflimsuplem7  44359  eliunxp2  45669