Theorem nfiu1 4960

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

Syntax hints:   ∈ wcel 2121  Ⅎwnfc 2888  ∃wrex 3065  ∪ ciun 4924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-rex 3066  df-v 3435  df-iun 4926

This theorem is referenced by:  ssiun2s  4981  disjxiun  5072  triun  5197  iunopeqop  5465  iunopeqopOLD  5466  eliunxp  5782  opeliunxp2  5783  opeliunxp2f  8154  ixpf  8862  ixpiunwdom  9499  r1val1  9705  rankuni2b  9772  rankval4  9786  cplem2  9809  ac6num  10396  iunfo  10456  iundom2g  10457  inar1  10693  tskuni  10701  gsum2d2lem  19943  gsum2d2  19944  gsumcom2  19945  iunconn  23415  ptclsg  23602  cnextfvval  24052  ssiun2sf  32652  djussxp2  32744  2ndresdju  32745  aciunf1lem  32758  fsumiunle  32925  suppgsumssiun  33157  irngnzply1  33887  esum2dlem  34288  esum2d  34289  esumiun  34290  sigapildsys  34358  bnj958  35137  bnj1000  35138  bnj981  35147  bnj1398  35231  bnj1408  35233  rankval4b  35296  ralssiun  37784  iunconnlem2  45393  iunmapss  45674  iunmapsn  45676  allbutfi  45851  fsumiunss  46034  dvnprodlem1  46403  dvnprodlem2  46404  sge0iunmptlemfi  46870  sge0iunmptlemre  46872  sge0iunmpt  46875  iundjiun  46917  voliunsge0lem  46929  caratheodorylem2  46984  smflimmpt  47267  smflimsuplem7  47283  eliunxp2  48839