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

Theorem dfiun2 4994
Description: Alternate definition of indexed union when 𝐵 is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 27-Jun-1998.) (Revised by David Abernethy, 19-Jun-2012.)
Hypothesis
Ref Expression
dfiun2.1 𝐵 ∈ V
Assertion
Ref Expression
dfiun2 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑦,𝐵
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem dfiun2
StepHypRef Expression
1 dfiun2g 4991 . 2 (∀𝑥𝐴 𝐵 ∈ V → 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
2 dfiun2.1 . . 3 𝐵 ∈ V
32a1i 11 . 2 (𝑥𝐴𝐵 ∈ V)
41, 3mprg 3067 1 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  {cab 2710  wrex 3070  Vcvv 3444   cuni 4866   ciun 4955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-11 2155  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-v 3446  df-uni 4867  df-iun 4957
This theorem is referenced by:  fniunfv  7195  funcnvuni  7869  fiun  7876  f1iun  7877  tfrlem8  8331  rdglim2a  8380  rankuni  9804  cardiun  9923  kmlem11  10101  cfslb2n  10209  enfin2i  10262  pwcfsdom  10524  rankcf  10718  tskuni  10724  discmp  22765  cmpsublem  22766  cmpsub  22767  nnoeomeqom  41690
  Copyright terms: Public domain W3C validator