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

Theorem dfiun2 5038
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 5035 . 2 (∀𝑥𝐴 𝐵 ∈ V → 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
2 dfiun2.1 . . 3 𝐵 ∈ V
32a1i 11 . 2 (𝑥𝐴𝐵 ∈ V)
41, 3mprg 3065 1 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  wcel 2106  {cab 2712  wrex 3068  Vcvv 3478   cuni 4912   ciun 4996
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-11 2155  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-v 3480  df-uni 4913  df-iun 4998
This theorem is referenced by:  fniunfv  7267  funcnvuni  7955  fiun  7966  f1iun  7967  tfrlem8  8423  rdglim2a  8472  rankuni  9901  cardiun  10020  kmlem11  10199  cfslb2n  10306  enfin2i  10359  pwcfsdom  10621  rankcf  10815  tskuni  10821  discmp  23422  cmpsublem  23423  cmpsub  23424  nnoeomeqom  43302
  Copyright terms: Public domain W3C validator