Theorem nfiu1 5003

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2157, ax-12 2177. (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 4971	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3267	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1853	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2886	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2108  Ⅎwnfc 2883  ∃wrex 3060  ∪ ciun 4967

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-rex 3061  df-v 3461  df-iun 4969

This theorem is referenced by:  ssiun2s  5024  disjxiun  5116  triun  5244  iunopeqop  5496  eliunxp  5817  opeliunxp2  5818  opeliunxp2f  8207  ixpf  8932  ixpiunwdom  9602  r1val1  9798  rankuni2b  9865  rankval4  9879  cplem2  9902  ac6num  10491  iunfo  10551  iundom2g  10552  inar1  10787  tskuni  10795  gsum2d2lem  19952  gsum2d2  19953  gsumcom2  19954  iunconn  23364  ptclsg  23551  cnextfvval  24001  ssiun2sf  32486  djussxp2  32572  2ndresdju  32573  aciunf1lem  32586  fsumiunle  32754  irngnzply1  33678  esum2dlem  34069  esum2d  34070  esumiun  34071  sigapildsys  34139  bnj958  34917  bnj1000  34918  bnj981  34927  bnj1398  35011  bnj1408  35013  ralssiun  37371  iunconnlem2  44907  iunmapss  45187  iunmapsn  45189  allbutfi  45368  fsumiunss  45552  dvnprodlem1  45923  dvnprodlem2  45924  sge0iunmptlemfi  46390  sge0iunmptlemre  46392  sge0iunmpt  46395  iundjiun  46437  voliunsge0lem  46449  caratheodorylem2  46504  smflimmpt  46787  smflimsuplem7  46803  eliunxp2  48257