Theorem nfiu1 5032

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 5000	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfre1 3283	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2910	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2902	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2107  {cab 2710  Ⅎwnfc 2884  ∃wrex 3071  ∪ ciun 4998

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rex 3072  df-iun 5000

This theorem is referenced by:  ssiun2s  5052  disjxiun  5146  triun  5281  iunopeqop  5522  eliunxp  5838  opeliunxp2  5839  opeliunxp2f  8195  ixpf  8914  ixpiunwdom  9585  r1val1  9781  rankuni2b  9848  rankval4  9862  cplem2  9885  ac6num  10474  iunfo  10534  iundom2g  10535  inar1  10770  tskuni  10778  gsum2d2lem  19841  gsum2d2  19842  gsumcom2  19843  iunconn  22932  ptclsg  23119  cnextfvval  23569  ssiun2sf  31791  djussxp2  31873  2ndresdju  31874  aciunf1lem  31887  fsumiunle  32035  irngnzply1  32755  esum2dlem  33090  esum2d  33091  esumiun  33092  sigapildsys  33160  bnj958  33951  bnj1000  33952  bnj981  33961  bnj1398  34045  bnj1408  34047  ralssiun  36288  iunconnlem2  43696  iunmapss  43914  iunmapsn  43916  allbutfi  44103  fsumiunss  44291  dvnprodlem1  44662  dvnprodlem2  44663  sge0iunmptlemfi  45129  sge0iunmptlemre  45131  sge0iunmpt  45134  iundjiun  45176  voliunsge0lem  45188  caratheodorylem2  45243  smflimmpt  45526  smflimsuplem7  45542  eliunxp2  47009