Theorem nfiu1 4994

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2195, ax-12 2216. (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 4962	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3292	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1886	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2915	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

This proof depends on syntax axioms:   ∈ wcel 2146  Ⅎwnfc 2912  ∃wrex 3091  ∪ ciun 4958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-rex 3092  df-v 3459  df-iun 4960

This theorem is used by:  ssiun2s  5015  disjxiun  5108  triun  5235  iunopeqop  5506  iunopeqopOLD  5507  eliunxp  5825  opeliunxp2  5826  opeliunxp2f  8212  ixpf  8924  ixpiunwdom  9559  r1val1  9765  rankuni2b  9832  rankval4  9846  cplem2  9888  cplem2OLD  9889  ac6num  10478  iunfo  10542  iundom2g  10543  inar1  10779  tskuni  10787  gsum2d2lem  20091  gsum2d2  20092  gsumcom2  20093  iunconn  23639  ptclsg  23827  cnextfvval  24277  ssiun2sf  32979  djussxp2  33068  2ndresdju  33069  aciunf1lem  33082  fsumiunle  33247  suppgsumssiun  33460  irngnzply1  34149  esum2dlem  34550  esum2d  34551  esumiun  34552  sigapildsys  34621  bnj958  35397  bnj1000  35398  bnj981  35407  bnj1398  35491  bnj1408  35493  rankval4b  35555  ralssiun  38114  iunconnlem2  45720  iunmapss  46008  iunmapsn  46010  allbutfi  46185  fsumiunss  46368  dvnprodlem1  46737  dvnprodlem2  46738  sge0iunmptlemfi  47204  sge0iunmptlemre  47206  sge0iunmpt  47209  iundjiun  47251  voliunsge0lem  47263  caratheodorylem2  47318  smflimmpt  47601  smflimsuplem7  47617  eliunxp2  49190