Theorem nfiu1 5030

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2147, ax-12 2167. (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 3279	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1848	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2882	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2099  Ⅎwnfc 2879  ∃wrex 3067  ∪ ciun 4996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-rex 3068  df-v 3473  df-iun 4998

This theorem is referenced by:  ssiun2s  5051  disjxiun  5145  triun  5280  iunopeqop  5523  eliunxp  5840  opeliunxp2  5841  opeliunxp2f  8216  ixpf  8939  ixpiunwdom  9614  r1val1  9810  rankuni2b  9877  rankval4  9891  cplem2  9914  ac6num  10503  iunfo  10563  iundom2g  10564  inar1  10799  tskuni  10807  gsum2d2lem  19928  gsum2d2  19929  gsumcom2  19930  iunconn  23345  ptclsg  23532  cnextfvval  23982  ssiun2sf  32363  djussxp2  32447  2ndresdju  32448  aciunf1lem  32461  fsumiunle  32605  irngnzply1  33369  esum2dlem  33711  esum2d  33712  esumiun  33713  sigapildsys  33781  bnj958  34571  bnj1000  34572  bnj981  34581  bnj1398  34665  bnj1408  34667  ralssiun  36886  iunconnlem2  44374  iunmapss  44588  iunmapsn  44590  allbutfi  44775  fsumiunss  44963  dvnprodlem1  45334  dvnprodlem2  45335  sge0iunmptlemfi  45801  sge0iunmptlemre  45803  sge0iunmpt  45806  iundjiun  45848  voliunsge0lem  45860  caratheodorylem2  45915  smflimmpt  46198  smflimsuplem7  46214  eliunxp2  47397