Theorem nfiu1 4970

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

Syntax hints:   ∈ wcel 2114  Ⅎwnfc 2884  ∃wrex 3062  ∪ ciun 4934

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 3063  df-v 3432  df-iun 4936

This theorem is referenced by:  ssiun2s  4992  disjxiun  5083  triun  5208  iunopeqop  5471  eliunxp  5788  opeliunxp2  5789  opeliunxp2f  8155  ixpf  8863  ixpiunwdom  9500  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  23407  ptclsg  23594  cnextfvval  24044  ssiun2sf  32648  djussxp2  32740  2ndresdju  32741  aciunf1lem  32754  fsumiunle  32921  suppgsumssiun  33152  irngnzply1  33855  esum2dlem  34256  esum2d  34257  esumiun  34258  sigapildsys  34326  bnj958  35102  bnj1000  35103  bnj981  35112  bnj1398  35196  bnj1408  35198  rankval4b  35263  ralssiun  37741  iunconnlem2  45383  iunmapss  45666  iunmapsn  45668  allbutfi  45844  fsumiunss  46027  dvnprodlem1  46396  dvnprodlem2  46397  sge0iunmptlemfi  46863  sge0iunmptlemre  46865  sge0iunmpt  46868  iundjiun  46910  voliunsge0lem  46922  caratheodorylem2  46977  smflimmpt  47260  smflimsuplem7  47276  eliunxp2  48826