Theorem nfiu1 4987

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2193, ax-12 2214. (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 4955	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3289	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1875	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2914	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2144  Ⅎwnfc 2911  ∃wrex 3088  ∪ ciun 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-nf 1806  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-rex 3089  df-v 3458  df-iun 4953

This theorem is referenced by:  ssiun2s  5008  disjxiun  5099  triun  5224  iunopeqop  5492  iunopeqopOLD  5493  eliunxp  5811  opeliunxp2  5812  opeliunxp2f  8192  ixpf  8904  ixpiunwdom  9540  r1val1  9746  rankuni2b  9813  rankval4  9827  cplem2  9850  ac6num  10438  iunfo  10498  iundom2g  10499  inar1  10735  tskuni  10743  gsum2d2lem  20015  gsum2d2  20016  gsumcom2  20017  iunconn  23490  ptclsg  23677  cnextfvval  24127  ssiun2sf  32761  djussxp2  32852  2ndresdju  32853  aciunf1lem  32866  fsumiunle  33033  suppgsumssiun  33254  irngnzply1  33990  esum2dlem  34391  esum2d  34392  esumiun  34393  sigapildsys  34461  bnj958  35237  bnj1000  35238  bnj981  35247  bnj1398  35331  bnj1408  35333  rankval4b  35400  ralssiun  37906  iunconnlem2  45515  iunmapss  45796  iunmapsn  45798  allbutfi  45973  fsumiunss  46156  dvnprodlem1  46525  dvnprodlem2  46526  sge0iunmptlemfi  46992  sge0iunmptlemre  46994  sge0iunmpt  46997  iundjiun  47039  voliunsge0lem  47051  caratheodorylem2  47106  smflimmpt  47389  smflimsuplem7  47405  eliunxp2  48961