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 3280	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	2	nfab 2907	. 2 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
4	1, 3	nfcxfr 2899	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2104  {cab 2707  Ⅎwnfc 2881  ∃wrex 3068  ∪ ciun 4998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-rex 3069  df-iun 5000

This theorem is referenced by:  ssiun2s  5052  disjxiun  5146  triun  5281  iunopeqop  5522  eliunxp  5838  opeliunxp2  5839  opeliunxp2f  8199  ixpf  8918  ixpiunwdom  9589  r1val1  9785  rankuni2b  9852  rankval4  9866  cplem2  9889  ac6num  10478  iunfo  10538  iundom2g  10539  inar1  10774  tskuni  10782  gsum2d2lem  19884  gsum2d2  19885  gsumcom2  19886  iunconn  23154  ptclsg  23341  cnextfvval  23791  ssiun2sf  32056  djussxp2  32138  2ndresdju  32139  aciunf1lem  32152  fsumiunle  32300  irngnzply1  33042  esum2dlem  33386  esum2d  33387  esumiun  33388  sigapildsys  33456  bnj958  34247  bnj1000  34248  bnj981  34257  bnj1398  34341  bnj1408  34343  ralssiun  36593  iunconnlem2  44000  iunmapss  44214  iunmapsn  44216  allbutfi  44403  fsumiunss  44591  dvnprodlem1  44962  dvnprodlem2  44963  sge0iunmptlemfi  45429  sge0iunmptlemre  45431  sge0iunmpt  45434  iundjiun  45476  voliunsge0lem  45488  caratheodorylem2  45543  smflimmpt  45826  smflimsuplem7  45842  eliunxp2  47099