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

Theorem nfiu1 4685
Description: Bound-variable hypothesis builder for indexed union. (Contributed by NM, 12-Oct-2003.)
Assertion
Ref Expression
nfiu1 𝑥 𝑥𝐴 𝐵

Proof of Theorem nfiu1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-iun 4657 . 2 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
2 nfre1 3153 . . 3 𝑥𝑥𝐴 𝑦𝐵
32nfab 2918 . 2 𝑥{𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
41, 3nfcxfr 2911 1 𝑥 𝑥𝐴 𝐵
Colors of variables: wff setvar class
Syntax hints:  wcel 2145  {cab 2757  wnfc 2900  wrex 3062   ciun 4655
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-iun 4657
This theorem is referenced by:  ssiun2s  4699  disjxiun  4784  triun  4900  iunopeqop  5115  eliunxp  5399  opeliunxp2  5400  opeliunxp2f  7489  ixpf  8085  ixpiunwdom  8653  r1val1  8814  rankuni2b  8881  rankval4  8895  cplem2  8918  ac6num  9504  iunfo  9564  iundom2g  9565  inar1  9800  tskuni  9808  gsum2d2lem  18580  gsum2d2  18581  gsumcom2  18582  iunconn  21453  ptclsg  21640  cnextfvval  22090  ssiun2sf  29717  aciunf1lem  29803  fsumiunle  29916  esum2dlem  30495  esum2d  30496  esumiun  30497  sigapildsys  30566  bnj958  31349  bnj1000  31350  bnj981  31359  bnj1398  31441  bnj1408  31443  iunconnlem2  39694  iunmapss  39926  iunmapsn  39928  allbutfi  40133  fsumiunss  40326  dvnprodlem1  40680  dvnprodlem2  40681  sge0iunmptlemfi  41148  sge0iunmptlemre  41150  sge0iunmpt  41153  iundjiun  41195  voliunsge0lem  41207  caratheodorylem2  41262  smflimmpt  41537  smflimsuplem7  41553  eliunxp2  42641
  Copyright terms: Public domain W3C validator