Theorem nfiu1 4977

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

Syntax hints:   ∈ wcel 2109  Ⅎwnfc 2876  ∃wrex 3053  ∪ ciun 4941

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rex 3054  df-v 3438  df-iun 4943

This theorem is referenced by:  ssiun2s  4997  disjxiun  5089  triun  5213  iunopeqop  5464  eliunxp  5780  opeliunxp2  5781  opeliunxp2f  8143  ixpf  8847  ixpiunwdom  9482  r1val1  9682  rankuni2b  9749  rankval4  9763  cplem2  9786  ac6num  10373  iunfo  10433  iundom2g  10434  inar1  10669  tskuni  10677  gsum2d2lem  19852  gsum2d2  19853  gsumcom2  19854  iunconn  23313  ptclsg  23500  cnextfvval  23950  ssiun2sf  32503  djussxp2  32592  2ndresdju  32593  aciunf1lem  32606  fsumiunle  32775  irngnzply1  33664  esum2dlem  34065  esum2d  34066  esumiun  34067  sigapildsys  34135  bnj958  34913  bnj1000  34914  bnj981  34923  bnj1398  35007  bnj1408  35009  ralssiun  37391  iunconnlem2  44918  iunmapss  45203  iunmapsn  45205  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  48328