Theorem nfiu1 5050

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2158, ax-12 2178. (Revised by SN, 14-May-2025.)

Assertion

Ref	Expression
nfiu1	⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Proof of Theorem nfiu1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eliun 5019	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3291	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1851	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2896	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2108  Ⅎwnfc 2893  ∃wrex 3076  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-rex 3077  df-v 3490  df-iun 5017

This theorem is referenced by:  ssiun2s  5071  disjxiun  5163  triun  5298  iunopeqop  5540  eliunxp  5862  opeliunxp2  5863  opeliunxp2f  8251  ixpf  8978  ixpiunwdom  9659  r1val1  9855  rankuni2b  9922  rankval4  9936  cplem2  9959  ac6num  10548  iunfo  10608  iundom2g  10609  inar1  10844  tskuni  10852  gsum2d2lem  20015  gsum2d2  20016  gsumcom2  20017  iunconn  23457  ptclsg  23644  cnextfvval  24094  ssiun2sf  32582  djussxp2  32666  2ndresdju  32667  aciunf1lem  32680  fsumiunle  32833  irngnzply1  33691  esum2dlem  34056  esum2d  34057  esumiun  34058  sigapildsys  34126  bnj958  34916  bnj1000  34917  bnj981  34926  bnj1398  35010  bnj1408  35012  ralssiun  37373  iunconnlem2  44906  iunmapss  45122  iunmapsn  45124  allbutfi  45308  fsumiunss  45496  dvnprodlem1  45867  dvnprodlem2  45868  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0iunmpt  46339  iundjiun  46381  voliunsge0lem  46393  caratheodorylem2  46448  smflimmpt  46731  smflimsuplem7  46747  eliunxp2  48058