Theorem nfiu1 5032

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

Syntax hints:   ∈ wcel 2106  Ⅎwnfc 2888  ∃wrex 3068  ∪ ciun 4996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-rex 3069  df-v 3480  df-iun 4998

This theorem is referenced by:  ssiun2s  5053  disjxiun  5145  triun  5280  iunopeqop  5531  eliunxp  5851  opeliunxp2  5852  opeliunxp2f  8234  ixpf  8959  ixpiunwdom  9628  r1val1  9824  rankuni2b  9891  rankval4  9905  cplem2  9928  ac6num  10517  iunfo  10577  iundom2g  10578  inar1  10813  tskuni  10821  gsum2d2lem  20006  gsum2d2  20007  gsumcom2  20008  iunconn  23452  ptclsg  23639  cnextfvval  24089  ssiun2sf  32580  djussxp2  32665  2ndresdju  32666  aciunf1lem  32679  fsumiunle  32836  irngnzply1  33706  esum2dlem  34073  esum2d  34074  esumiun  34075  sigapildsys  34143  bnj958  34933  bnj1000  34934  bnj981  34943  bnj1398  35027  bnj1408  35029  ralssiun  37390  iunconnlem2  44933  iunmapss  45158  iunmapsn  45160  allbutfi  45343  fsumiunss  45531  dvnprodlem1  45902  dvnprodlem2  45903  sge0iunmptlemfi  46369  sge0iunmptlemre  46371  sge0iunmpt  46374  iundjiun  46416  voliunsge0lem  46428  caratheodorylem2  46483  smflimmpt  46766  smflimsuplem7  46782  eliunxp2  48179