Theorem nfiu1 4915

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 4883	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfre1 3265	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2961	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2953	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2111  {cab 2776  Ⅎwnfc 2936  ∃wrex 3107  ∪ ciun 4881

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 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rex 3112  df-iun 4883

This theorem is referenced by:  ssiun2s  4935  disjxiun  5027  triun  5149  iunopeqop  5376  eliunxp  5672  opeliunxp2  5673  opeliunxp2f  7859  ixpf  8467  ixpiunwdom  9038  r1val1  9199  rankuni2b  9266  rankval4  9280  cplem2  9303  ac6num  9890  iunfo  9950  iundom2g  9951  inar1  10186  tskuni  10194  gsum2d2lem  19086  gsum2d2  19087  gsumcom2  19088  iunconn  22033  ptclsg  22220  cnextfvval  22670  ssiun2sf  30323  djussxp2  30410  2ndresdju  30411  aciunf1lem  30425  fsumiunle  30571  esum2dlem  31461  esum2d  31462  esumiun  31463  sigapildsys  31531  bnj958  32322  bnj1000  32323  bnj981  32332  bnj1398  32416  bnj1408  32418  ralssiun  34824  iunconnlem2  41641  iunmapss  41844  iunmapsn  41846  allbutfi  42029  fsumiunss  42217  dvnprodlem1  42588  dvnprodlem2  42589  sge0iunmptlemfi  43052  sge0iunmptlemre  43054  sge0iunmpt  43057  iundjiun  43099  voliunsge0lem  43111  caratheodorylem2  43166  smflimmpt  43441  smflimsuplem7  43457  eliunxp2  44735