Theorem nfiu1 4975

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2160, ax-12 2180. (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 4943	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3257	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1854	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2882	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2111  Ⅎwnfc 2879  ∃wrex 3056  ∪ ciun 4939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-rex 3057  df-v 3438  df-iun 4941

This theorem is referenced by:  ssiun2s  4995  disjxiun  5086  triun  5210  iunopeqop  5459  eliunxp  5776  opeliunxp2  5777  opeliunxp2f  8140  ixpf  8844  ixpiunwdom  9476  r1val1  9679  rankuni2b  9746  rankval4  9760  cplem2  9783  ac6num  10370  iunfo  10430  iundom2g  10431  inar1  10666  tskuni  10674  gsum2d2lem  19885  gsum2d2  19886  gsumcom2  19887  iunconn  23343  ptclsg  23530  cnextfvval  23980  ssiun2sf  32539  djussxp2  32630  2ndresdju  32631  aciunf1lem  32644  fsumiunle  32812  irngnzply1  33704  esum2dlem  34105  esum2d  34106  esumiun  34107  sigapildsys  34175  bnj958  34952  bnj1000  34953  bnj981  34962  bnj1398  35046  bnj1408  35048  rankval4b  35111  ralssiun  37451  iunconnlem2  45026  iunmapss  45311  iunmapsn  45313  allbutfi  45490  fsumiunss  45674  dvnprodlem1  46043  dvnprodlem2  46044  sge0iunmptlemfi  46510  sge0iunmptlemre  46512  sge0iunmpt  46515  iundjiun  46557  voliunsge0lem  46569  caratheodorylem2  46624  smflimmpt  46907  smflimsuplem7  46923  eliunxp2  48433