Theorem nfiu1 4992

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

This proof depends on syntax axioms:   ∈ wcel 2143  Ⅎwnfc 2910  ∃wrex 3089  ∪ ciun 4956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-rex 3090  df-v 3457  df-iun 4958

This theorem is used by:  ssiun2s  5013  disjxiun  5106  triun  5233  iunopeqop  5504  iunopeqopOLD  5505  eliunxp  5823  opeliunxp2  5824  opeliunxp2f  8202  ixpf  8914  ixpiunwdom  9548  r1val1  9754  rankuni2b  9821  rankval4  9835  cplem2  9877  cplem2OLD  9878  ac6num  10467  iunfo  10527  iundom2g  10528  inar1  10764  tskuni  10772  gsum2d2lem  20047  gsum2d2  20048  gsumcom2  20049  iunconn  23594  ptclsg  23781  cnextfvval  24231  ssiun2sf  32913  djussxp2  33002  2ndresdju  33003  aciunf1lem  33016  fsumiunle  33182  suppgsumssiun  33401  irngnzply1  34090  esum2dlem  34491  esum2d  34492  esumiun  34493  sigapildsys  34561  bnj958  35337  bnj1000  35338  bnj981  35347  bnj1398  35431  bnj1408  35433  rankval4b  35502  ralssiun  38081  iunconnlem2  45671  iunmapss  45959  iunmapsn  45961  allbutfi  46136  fsumiunss  46319  dvnprodlem1  46688  dvnprodlem2  46689  sge0iunmptlemfi  47155  sge0iunmptlemre  47157  sge0iunmpt  47160  iundjiun  47202  voliunsge0lem  47214  caratheodorylem2  47269  smflimmpt  47552  smflimsuplem7  47568  eliunxp2  49142