Theorem nfiu1 4817

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 4788	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2		nfre1 3245	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2932	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2924	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2048  {cab 2753  Ⅎwnfc 2910  ∃wrex 3083  ∪ ciun 4786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rex 3088  df-iun 4788

This theorem is referenced by:  ssiun2s  4832  disjxiun  4920  triun  5037  iunopeqop  5260  eliunxp  5551  opeliunxp2  5552  opeliunxp2f  7672  ixpf  8273  ixpiunwdom  8842  r1val1  9001  rankuni2b  9068  rankval4  9082  cplem2  9105  ac6num  9691  iunfo  9751  iundom2g  9752  inar1  9987  tskuni  9995  gsum2d2lem  18836  gsum2d2  18837  gsumcom2  18838  iunconn  21730  ptclsg  21917  cnextfvval  22367  ssiun2sf  30070  aciunf1lem  30159  fsumiunle  30280  esum2dlem  30952  esum2d  30953  esumiun  30954  sigapildsys  31023  bnj958  31820  bnj1000  31821  bnj981  31830  bnj1398  31912  bnj1408  31914  ralssiun  34064  iunconnlem2  40632  iunmapss  40849  iunmapsn  40851  allbutfi  41041  fsumiunss  41233  dvnprodlem1  41607  dvnprodlem2  41608  sge0iunmptlemfi  42072  sge0iunmptlemre  42074  sge0iunmpt  42077  iundjiun  42119  voliunsge0lem  42131  caratheodorylem2  42186  smflimmpt  42461  smflimsuplem7  42477  eliunxp2  43686