Theorem nfiu1 4980

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

Syntax hints:   ∈ wcel 2113  Ⅎwnfc 2881  ∃wrex 3058  ∪ ciun 4944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-rex 3059  df-v 3440  df-iun 4946

This theorem is referenced by:  ssiun2s  5002  disjxiun  5093  triun  5217  iunopeqop  5467  eliunxp  5784  opeliunxp2  5785  opeliunxp2f  8150  ixpf  8856  ixpiunwdom  9493  r1val1  9696  rankuni2b  9763  rankval4  9777  cplem2  9800  ac6num  10387  iunfo  10447  iundom2g  10448  inar1  10684  tskuni  10692  gsum2d2lem  19900  gsum2d2  19901  gsumcom2  19902  iunconn  23370  ptclsg  23557  cnextfvval  24007  ssiun2sf  32583  djussxp2  32675  2ndresdju  32676  aciunf1lem  32689  fsumiunle  32859  irngnzply1  33797  esum2dlem  34198  esum2d  34199  esumiun  34200  sigapildsys  34268  bnj958  35045  bnj1000  35046  bnj981  35055  bnj1398  35139  bnj1408  35141  rankval4b  35205  ralssiun  37551  iunconnlem2  45117  iunmapss  45401  iunmapsn  45403  allbutfi  45579  fsumiunss  45763  dvnprodlem1  46132  dvnprodlem2  46133  sge0iunmptlemfi  46599  sge0iunmptlemre  46601  sge0iunmpt  46604  iundjiun  46646  voliunsge0lem  46658  caratheodorylem2  46713  smflimmpt  46996  smflimsuplem7  47012  eliunxp2  48522