Theorem nfiu1 4989

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2196, ax-12 2215. (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 4958	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3291	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1885	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2914	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

This proof depends on syntax axioms:   ∈ wcel 2146  Ⅎwnfc 2911  ∃wrex 3090  ∪ ciun 4954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-rex 3091  df-v 3456  df-iun 4956

This theorem is used by:  ssiun2s  5010  disjxiun  5103  triun  5230  iunopeqop  5498  iunopeqopOLD  5499  eliunxp  5819  opeliunxp2  5820  opeliunxp2f  8241  ixpf  8962  ixpiunwdom  9597  r1val1  9806  rankuni2b  9880  rankval4b  9893  rankval4  9897  cplem2  9965  cplem2OLD  9966  ac6num  10570  iunfo  10636  iundom2g  10637  inar1  10873  tskuni  10881  gsum2d2lem  20202  gsum2d2  20203  gsumcom2  20204  iunconn  23761  ptclsg  23949  cnextfvval  24399  ssiun2sf  33211  djussxp2  33299  2ndresdju  33300  aciunf1lem  33313  fsumiunle  33476  suppgsumssiun  33689  irngnzply1  34379  esum2dlem  34780  esum2d  34781  esumiun  34782  sigapildsys  34851  bnj958  35626  bnj1000  35627  bnj981  35636  bnj1398  35720  bnj1408  35722  ralssiun  38473  iunconnlem2  46059  iunmapss  46370  iunmapsn  46372  allbutfi  46546  fsumiunss  46729  dvnprodlem1  47098  dvnprodlem2  47099  sge0iunmptlemfi  47565  sge0iunmptlemre  47567  sge0iunmpt  47570  iundjiun  47612  voliunsge0lem  47624  caratheodorylem2  47679  smflimmpt  47962  smflimsuplem7  47978  eliunxp2  49588