Theorem nfiu1 4984

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2163, ax-12 2185. (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 4952	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3263	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1855	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2887	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2114  Ⅎwnfc 2884  ∃wrex 3062  ∪ ciun 4948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rex 3063  df-v 3444  df-iun 4950

This theorem is referenced by:  ssiun2s  5006  disjxiun  5097  triun  5221  iunopeqop  5479  eliunxp  5796  opeliunxp2  5797  opeliunxp2f  8164  ixpf  8872  ixpiunwdom  9509  r1val1  9712  rankuni2b  9779  rankval4  9793  cplem2  9816  ac6num  10403  iunfo  10463  iundom2g  10464  inar1  10700  tskuni  10708  gsum2d2lem  19919  gsum2d2  19920  gsumcom2  19921  iunconn  23389  ptclsg  23576  cnextfvval  24026  ssiun2sf  32652  djussxp2  32744  2ndresdju  32745  aciunf1lem  32758  fsumiunle  32927  suppgsumssiun  33172  irngnzply1  33875  esum2dlem  34276  esum2d  34277  esumiun  34278  sigapildsys  34346  bnj958  35122  bnj1000  35123  bnj981  35132  bnj1398  35216  bnj1408  35218  rankval4b  35283  ralssiun  37689  iunconnlem2  45319  iunmapss  45602  iunmapsn  45604  allbutfi  45780  fsumiunss  45964  dvnprodlem1  46333  dvnprodlem2  46334  sge0iunmptlemfi  46800  sge0iunmptlemre  46802  sge0iunmpt  46805  iundjiun  46847  voliunsge0lem  46859  caratheodorylem2  46914  smflimmpt  47197  smflimsuplem7  47213  eliunxp2  48723