Theorem nfiu1 5026

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2156, ax-12 2176. (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 4994	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3284	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1852	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2892	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2107  Ⅎwnfc 2889  ∃wrex 3069  ∪ ciun 4990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-rex 3070  df-v 3481  df-iun 4992

This theorem is referenced by:  ssiun2s  5047  disjxiun  5139  triun  5273  iunopeqop  5525  eliunxp  5847  opeliunxp2  5848  opeliunxp2f  8236  ixpf  8961  ixpiunwdom  9631  r1val1  9827  rankuni2b  9894  rankval4  9908  cplem2  9931  ac6num  10520  iunfo  10580  iundom2g  10581  inar1  10816  tskuni  10824  gsum2d2lem  19992  gsum2d2  19993  gsumcom2  19994  iunconn  23437  ptclsg  23624  cnextfvval  24074  ssiun2sf  32573  djussxp2  32659  2ndresdju  32660  aciunf1lem  32673  fsumiunle  32832  irngnzply1  33742  esum2dlem  34094  esum2d  34095  esumiun  34096  sigapildsys  34164  bnj958  34955  bnj1000  34956  bnj981  34965  bnj1398  35049  bnj1408  35051  ralssiun  37409  iunconnlem2  44960  iunmapss  45225  iunmapsn  45227  allbutfi  45409  fsumiunss  45595  dvnprodlem1  45966  dvnprodlem2  45967  sge0iunmptlemfi  46433  sge0iunmptlemre  46435  sge0iunmpt  46438  iundjiun  46480  voliunsge0lem  46492  caratheodorylem2  46547  smflimmpt  46830  smflimsuplem7  46846  eliunxp2  48255