Theorem nfiu1 4987

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 4955	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3260	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1853	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2879	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2109  Ⅎwnfc 2876  ∃wrex 3053  ∪ ciun 4951

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rex 3054  df-v 3446  df-iun 4953

This theorem is referenced by:  ssiun2s  5007  disjxiun  5099  triun  5224  iunopeqop  5476  eliunxp  5791  opeliunxp2  5792  opeliunxp2f  8166  ixpf  8870  ixpiunwdom  9519  r1val1  9715  rankuni2b  9782  rankval4  9796  cplem2  9819  ac6num  10408  iunfo  10468  iundom2g  10469  inar1  10704  tskuni  10712  gsum2d2lem  19887  gsum2d2  19888  gsumcom2  19889  iunconn  23348  ptclsg  23535  cnextfvval  23985  ssiun2sf  32538  djussxp2  32622  2ndresdju  32623  aciunf1lem  32636  fsumiunle  32804  irngnzply1  33679  esum2dlem  34075  esum2d  34076  esumiun  34077  sigapildsys  34145  bnj958  34923  bnj1000  34924  bnj981  34933  bnj1398  35017  bnj1408  35019  ralssiun  37388  iunconnlem2  44917  iunmapss  45202  iunmapsn  45204  allbutfi  45382  fsumiunss  45566  dvnprodlem1  45937  dvnprodlem2  45938  sge0iunmptlemfi  46404  sge0iunmptlemre  46406  sge0iunmpt  46409  iundjiun  46451  voliunsge0lem  46463  caratheodorylem2  46518  smflimmpt  46801  smflimsuplem7  46817  eliunxp2  48315