MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfiu1 Structured version   Visualization version   GIF version

Theorem nfiu1 5030
Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.) Avoid ax-11 2147, ax-12 2167. (Revised by SN, 14-May-2025.)
Assertion
Ref Expression
nfiu1 𝑥 𝑥𝐴 𝐵

Proof of Theorem nfiu1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eliun 5000 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑦𝐵)
2 nfre1 3279 . . 3 𝑥𝑥𝐴 𝑦𝐵
31, 2nfxfr 1848 . 2 𝑥 𝑦 𝑥𝐴 𝐵
43nfci 2882 1 𝑥 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2099  wnfc 2879  wrex 3067   ciun 4996
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-rex 3068  df-v 3473  df-iun 4998
This theorem is referenced by:  ssiun2s  5051  disjxiun  5145  triun  5280  iunopeqop  5523  eliunxp  5840  opeliunxp2  5841  opeliunxp2f  8216  ixpf  8939  ixpiunwdom  9614  r1val1  9810  rankuni2b  9877  rankval4  9891  cplem2  9914  ac6num  10503  iunfo  10563  iundom2g  10564  inar1  10799  tskuni  10807  gsum2d2lem  19928  gsum2d2  19929  gsumcom2  19930  iunconn  23345  ptclsg  23532  cnextfvval  23982  ssiun2sf  32363  djussxp2  32447  2ndresdju  32448  aciunf1lem  32461  fsumiunle  32605  irngnzply1  33369  esum2dlem  33711  esum2d  33712  esumiun  33713  sigapildsys  33781  bnj958  34571  bnj1000  34572  bnj981  34581  bnj1398  34665  bnj1408  34667  ralssiun  36886  iunconnlem2  44374  iunmapss  44588  iunmapsn  44590  allbutfi  44775  fsumiunss  44963  dvnprodlem1  45334  dvnprodlem2  45335  sge0iunmptlemfi  45801  sge0iunmptlemre  45803  sge0iunmpt  45806  iundjiun  45848  voliunsge0lem  45860  caratheodorylem2  45915  smflimmpt  46198  smflimsuplem7  46214  eliunxp2  47397
  Copyright terms: Public domain W3C validator