Theorem nfiu1 4986

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

This proof depends on syntax axioms:   ∈ wcel 2145  Ⅎwnfc 2907  ∃wrex 3086  ∪ ciun 4951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-rex 3087  df-v 3452  df-iun 4953

This theorem is used by:  ssiun2s  5007  disjxiun  5100  triun  5227  iunopeqop  5498  iunopeqopOLD  5499  eliunxp  5817  opeliunxp2  5818  opeliunxp2f  8209  ixpf  8930  ixpiunwdom  9565  r1val1  9771  rankuni2b  9838  rankval4  9852  cplem2  9894  cplem2OLD  9895  ac6num  10484  iunfo  10550  iundom2g  10551  inar1  10787  tskuni  10795  gsum2d2lem  20103  gsum2d2  20104  gsumcom2  20105  iunconn  23656  ptclsg  23844  cnextfvval  24294  ssiun2sf  33036  djussxp2  33124  2ndresdju  33125  aciunf1lem  33138  fsumiunle  33302  suppgsumssiun  33515  irngnzply1  34204  esum2dlem  34605  esum2d  34606  esumiun  34607  sigapildsys  34676  bnj958  35452  bnj1000  35453  bnj981  35462  bnj1398  35546  bnj1408  35548  rankval4b  35610  ralssiun  38164  iunconnlem2  45760  iunmapss  46048  iunmapsn  46050  allbutfi  46225  fsumiunss  46408  dvnprodlem1  46777  dvnprodlem2  46778  sge0iunmptlemfi  47244  sge0iunmptlemre  47246  sge0iunmpt  47249  iundjiun  47291  voliunsge0lem  47303  caratheodorylem2  47358  smflimmpt  47641  smflimsuplem7  47657  eliunxp2  49267