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 3288	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1886	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2911	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

This proof depends on syntax axioms:   ∈ wcel 2145  Ⅎwnfc 2908  ∃wrex 3087  ∪ 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 2733

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 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-rex 3088  df-v 3453  df-iun 4953

This theorem is used by:  ssiun2s  5007  disjxiun  5100  triun  5227  iunopeqop  5494  iunopeqopOLD  5495  eliunxp  5814  opeliunxp2  5815  opeliunxp2f  8227  ixpf  8948  ixpiunwdom  9584  r1val1  9793  rankuni2b  9867  rankval4b  9880  rankval4  9884  cplem2  9952  cplem2OLD  9953  ac6num  10557  iunfo  10623  iundom2g  10624  inar1  10860  tskuni  10868  gsum2d2lem  20187  gsum2d2  20188  gsumcom2  20189  iunconn  23746  ptclsg  23934  cnextfvval  24384  ssiun2sf  33154  djussxp2  33242  2ndresdju  33243  aciunf1lem  33256  fsumiunle  33420  suppgsumssiun  33633  irngnzply1  34323  esum2dlem  34724  esum2d  34725  esumiun  34726  sigapildsys  34795  bnj958  35570  bnj1000  35571  bnj981  35580  bnj1398  35664  bnj1408  35666  ralssiun  38330  iunconnlem2  45916  iunmapss  46227  iunmapsn  46229  allbutfi  46403  fsumiunss  46586  dvnprodlem1  46955  dvnprodlem2  46956  sge0iunmptlemfi  47422  sge0iunmptlemre  47424  sge0iunmpt  47427  iundjiun  47469  voliunsge0lem  47481  caratheodorylem2  47536  smflimmpt  47819  smflimsuplem7  47835  eliunxp2  49445