Theorem nfiu1 4983

Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2163, ax-12 2185. (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 4951	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3262	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1855	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2887	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2114  Ⅎwnfc 2884  ∃wrex 3061  ∪ ciun 4947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-rex 3062  df-v 3443  df-iun 4949

This theorem is referenced by:  ssiun2s  5005  disjxiun  5096  triun  5220  iunopeqop  5470  eliunxp  5787  opeliunxp2  5788  opeliunxp2f  8154  ixpf  8862  ixpiunwdom  9499  r1val1  9702  rankuni2b  9769  rankval4  9783  cplem2  9806  ac6num  10393  iunfo  10453  iundom2g  10454  inar1  10690  tskuni  10698  gsum2d2lem  19906  gsum2d2  19907  gsumcom2  19908  iunconn  23376  ptclsg  23563  cnextfvval  24013  ssiun2sf  32637  djussxp2  32729  2ndresdju  32730  aciunf1lem  32743  fsumiunle  32912  irngnzply1  33850  esum2dlem  34251  esum2d  34252  esumiun  34253  sigapildsys  34321  bnj958  35098  bnj1000  35099  bnj981  35108  bnj1398  35192  bnj1408  35194  rankval4b  35258  ralssiun  37614  iunconnlem2  45242  iunmapss  45526  iunmapsn  45528  allbutfi  45704  fsumiunss  45888  dvnprodlem1  46257  dvnprodlem2  46258  sge0iunmptlemfi  46724  sge0iunmptlemre  46726  sge0iunmpt  46729  iundjiun  46771  voliunsge0lem  46783  caratheodorylem2  46838  smflimmpt  47121  smflimsuplem7  47137  eliunxp2  48647