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

Theorem nfiu1 4694
 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 4666 . 2 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
2 nfre1 3135 . . 3 𝑥𝑥𝐴 𝑦𝐵
32nfab 2899 . 2 𝑥{𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
41, 3nfcxfr 2892 1 𝑥 𝑥𝐴 𝐵
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2131  {cab 2738  Ⅎwnfc 2881  ∃wrex 3043  ∪ ciun 4664 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rex 3048  df-iun 4666 This theorem is referenced by:  ssiun2s  4708  disjxiun  4793  triun  4910  iunopeqop  5123  eliunxp  5407  opeliunxp2  5408  opeliunxp2f  7497  ixpf  8088  ixpiunwdom  8653  r1val1  8814  rankuni2b  8881  rankval4  8895  cplem2  8918  ac6num  9485  iunfo  9545  iundom2g  9546  inar1  9781  tskuni  9789  gsum2d2lem  18564  gsum2d2  18565  gsumcom2  18566  iunconn  21425  ptclsg  21612  cnextfvval  22062  ssiun2sf  29677  aciunf1lem  29763  fsumiunle  29876  esum2dlem  30455  esum2d  30456  esumiun  30457  sigapildsys  30526  bnj958  31309  bnj1000  31310  bnj981  31319  bnj1398  31401  bnj1408  31403  iunconnlem2  39662  iunmapss  39898  iunmapsn  39900  allbutfi  40106  fsumiunss  40302  dvnprodlem1  40656  dvnprodlem2  40657  sge0iunmptlemfi  41125  sge0iunmptlemre  41127  sge0iunmpt  41130  iundjiun  41172  voliunsge0lem  41184  caratheodorylem2  41239  smflimmpt  41514  smflimsuplem7  41530  eliunxp2  42614
 Copyright terms: Public domain W3C validator