Theorem nfiu1 4993

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

Syntax hints:   ∈ wcel 2109  Ⅎwnfc 2877  ∃wrex 3054  ∪ ciun 4957

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-rex 3055  df-v 3452  df-iun 4959

This theorem is referenced by:  ssiun2s  5014  disjxiun  5106  triun  5231  iunopeqop  5483  eliunxp  5803  opeliunxp2  5804  opeliunxp2f  8191  ixpf  8895  ixpiunwdom  9549  r1val1  9745  rankuni2b  9812  rankval4  9826  cplem2  9849  ac6num  10438  iunfo  10498  iundom2g  10499  inar1  10734  tskuni  10742  gsum2d2lem  19909  gsum2d2  19910  gsumcom2  19911  iunconn  23321  ptclsg  23508  cnextfvval  23958  ssiun2sf  32494  djussxp2  32578  2ndresdju  32579  aciunf1lem  32592  fsumiunle  32760  irngnzply1  33692  esum2dlem  34088  esum2d  34089  esumiun  34090  sigapildsys  34158  bnj958  34936  bnj1000  34937  bnj981  34946  bnj1398  35030  bnj1408  35032  ralssiun  37390  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  48312