Theorem nfiu1 4996

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2198, ax-12 2219. (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 4964	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3296	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1880	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2919	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2149  Ⅎwnfc 2916  ∃wrex 3095  ∪ ciun 4960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-rex 3096  df-v 3465  df-iun 4962

This theorem is referenced by:  ssiun2s  5017  disjxiun  5110  triun  5237  iunopeqop  5505  iunopeqopOLD  5506  eliunxp  5824  opeliunxp2  5825  opeliunxp2f  8206  ixpf  8918  ixpiunwdom  9552  r1val1  9758  rankuni2b  9825  rankval4  9839  cplem2  9876  ac6num  10463  iunfo  10523  iundom2g  10524  inar1  10760  tskuni  10768  gsum2d2lem  20043  gsum2d2  20044  gsumcom2  20045  iunconn  23554  ptclsg  23741  cnextfvval  24191  ssiun2sf  32845  djussxp2  32934  2ndresdju  32935  aciunf1lem  32948  fsumiunle  33114  suppgsumssiun  33333  irngnzply1  34026  esum2dlem  34427  esum2d  34428  esumiun  34429  sigapildsys  34497  bnj958  35273  bnj1000  35274  bnj981  35283  bnj1398  35367  bnj1408  35369  rankval4b  35436  ralssiun  37975  iunconnlem2  45569  iunmapss  45857  iunmapsn  45859  allbutfi  46034  fsumiunss  46217  dvnprodlem1  46586  dvnprodlem2  46587  sge0iunmptlemfi  47053  sge0iunmptlemre  47055  sge0iunmpt  47058  iundjiun  47100  voliunsge0lem  47112  caratheodorylem2  47167  smflimmpt  47450  smflimsuplem7  47466  eliunxp2  49033