Theorem nfiu1 4969

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 4937	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
2		nfre1 3262	. . 3 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
3	1, 2	nfxfr 1855	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
4	3	nfci 2886	1 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵

Syntax hints:   ∈ wcel 2114  Ⅎwnfc 2883  ∃wrex 3061  ∪ ciun 4933

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-rex 3062  df-v 3431  df-iun 4935

This theorem is referenced by:  ssiun2s  4991  disjxiun  5082  triun  5207  iunopeqop  5475  iunopeqopOLD  5476  eliunxp  5792  opeliunxp2  5793  opeliunxp2f  8160  ixpf  8868  ixpiunwdom  9505  r1val1  9710  rankuni2b  9777  rankval4  9791  cplem2  9814  ac6num  10401  iunfo  10461  iundom2g  10462  inar1  10698  tskuni  10706  gsum2d2lem  19948  gsum2d2  19949  gsumcom2  19950  iunconn  23393  ptclsg  23580  cnextfvval  24030  ssiun2sf  32629  djussxp2  32721  2ndresdju  32722  aciunf1lem  32735  fsumiunle  32902  suppgsumssiun  33133  irngnzply1  33835  esum2dlem  34236  esum2d  34237  esumiun  34238  sigapildsys  34306  bnj958  35082  bnj1000  35083  bnj981  35092  bnj1398  35176  bnj1408  35178  rankval4b  35243  ralssiun  37723  iunconnlem2  45361  iunmapss  45644  iunmapsn  45646  allbutfi  45822  fsumiunss  46005  dvnprodlem1  46374  dvnprodlem2  46375  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0iunmpt  46846  iundjiun  46888  voliunsge0lem  46900  caratheodorylem2  46955  smflimmpt  47238  smflimsuplem7  47254  eliunxp2  48810