Theorem nfiu1 5053

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2153, ax-12 2173. (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 5023	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3286	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1851	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2891	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2103  Ⅎwnfc 2888  ∃wrex 3072  ∪ ciun 5019

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-rex 3073  df-v 3484  df-iun 5021

This theorem is referenced by:  ssiun2s  5074  disjxiun  5166  triun  5301  iunopeqop  5544  eliunxp  5861  opeliunxp2  5862  opeliunxp2f  8247  ixpf  8974  ixpiunwdom  9655  r1val1  9851  rankuni2b  9918  rankval4  9932  cplem2  9955  ac6num  10544  iunfo  10604  iundom2g  10605  inar1  10840  tskuni  10848  gsum2d2lem  20010  gsum2d2  20011  gsumcom2  20012  iunconn  23450  ptclsg  23637  cnextfvval  24087  ssiun2sf  32573  djussxp2  32658  2ndresdju  32659  aciunf1lem  32672  fsumiunle  32825  irngnzply1  33683  esum2dlem  34048  esum2d  34049  esumiun  34050  sigapildsys  34118  bnj958  34908  bnj1000  34909  bnj981  34918  bnj1398  35002  bnj1408  35004  weiunfrlem2  36380  ralssiun  37321  iunconnlem2  44846  iunmapss  45056  iunmapsn  45058  allbutfi  45242  fsumiunss  45430  dvnprodlem1  45801  dvnprodlem2  45802  sge0iunmptlemfi  46268  sge0iunmptlemre  46270  sge0iunmpt  46273  iundjiun  46315  voliunsge0lem  46327  caratheodorylem2  46382  smflimmpt  46665  smflimsuplem7  46681  eliunxp2  47976