Theorem nfiu1 5008

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

Syntax hints:   ∈ wcel 2109  Ⅎwnfc 2884  ∃wrex 3061  ∪ ciun 4972

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-rex 3062  df-v 3466  df-iun 4974

This theorem is referenced by:  ssiun2s  5029  disjxiun  5121  triun  5249  iunopeqop  5501  eliunxp  5822  opeliunxp2  5823  opeliunxp2f  8214  ixpf  8939  ixpiunwdom  9609  r1val1  9805  rankuni2b  9872  rankval4  9886  cplem2  9909  ac6num  10498  iunfo  10558  iundom2g  10559  inar1  10794  tskuni  10802  gsum2d2lem  19959  gsum2d2  19960  gsumcom2  19961  iunconn  23371  ptclsg  23558  cnextfvval  24008  ssiun2sf  32545  djussxp2  32631  2ndresdju  32632  aciunf1lem  32645  fsumiunle  32813  irngnzply1  33737  esum2dlem  34128  esum2d  34129  esumiun  34130  sigapildsys  34198  bnj958  34976  bnj1000  34977  bnj981  34986  bnj1398  35070  bnj1408  35072  ralssiun  37430  iunconnlem2  44934  iunmapss  45219  iunmapsn  45221  allbutfi  45400  fsumiunss  45584  dvnprodlem1  45955  dvnprodlem2  45956  sge0iunmptlemfi  46422  sge0iunmptlemre  46424  sge0iunmpt  46427  iundjiun  46469  voliunsge0lem  46481  caratheodorylem2  46536  smflimmpt  46819  smflimsuplem7  46835  eliunxp2  48289