Theorem nfiu1 4993

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 4961	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfre1 3266	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2908	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2900	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2106  {cab 2708  Ⅎwnfc 2882  ∃wrex 3069  ∪ ciun 4959

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-rex 3070  df-iun 4961

This theorem is referenced by:  ssiun2s  5013  disjxiun  5107  triun  5242  iunopeqop  5483  eliunxp  5798  opeliunxp2  5799  opeliunxp2f  8146  ixpf  8865  ixpiunwdom  9535  r1val1  9731  rankuni2b  9798  rankval4  9812  cplem2  9835  ac6num  10424  iunfo  10484  iundom2g  10485  inar1  10720  tskuni  10728  gsum2d2lem  19764  gsum2d2  19765  gsumcom2  19766  iunconn  22816  ptclsg  23003  cnextfvval  23453  ssiun2sf  31545  djussxp2  31631  2ndresdju  31632  aciunf1lem  31645  fsumiunle  31795  irngnzply1  32452  esum2dlem  32780  esum2d  32781  esumiun  32782  sigapildsys  32850  bnj958  33641  bnj1000  33642  bnj981  33651  bnj1398  33735  bnj1408  33737  ralssiun  35951  iunconnlem2  43339  iunmapss  43557  iunmapsn  43559  allbutfi  43748  fsumiunss  43936  dvnprodlem1  44307  dvnprodlem2  44308  sge0iunmptlemfi  44774  sge0iunmptlemre  44776  sge0iunmpt  44779  iundjiun  44821  voliunsge0lem  44833  caratheodorylem2  44888  smflimmpt  45171  smflimsuplem7  45187  eliunxp2  46529