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

Theorem dfiun2g 4488
 Description: Alternate definition of indexed union when 𝐵 is a set. Definition 15(a) of [Suppes] p. 44. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
dfiun2g (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥,𝑦)

Proof of Theorem dfiun2g
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nfra1 2925 . . . . . 6 𝑥𝑥𝐴 𝐵𝐶
2 rsp 2913 . . . . . . . 8 (∀𝑥𝐴 𝐵𝐶 → (𝑥𝐴𝐵𝐶))
3 clel3g 3310 . . . . . . . 8 (𝐵𝐶 → (𝑧𝐵 ↔ ∃𝑦(𝑦 = 𝐵𝑧𝑦)))
42, 3syl6 34 . . . . . . 7 (∀𝑥𝐴 𝐵𝐶 → (𝑥𝐴 → (𝑧𝐵 ↔ ∃𝑦(𝑦 = 𝐵𝑧𝑦))))
54imp 444 . . . . . 6 ((∀𝑥𝐴 𝐵𝐶𝑥𝐴) → (𝑧𝐵 ↔ ∃𝑦(𝑦 = 𝐵𝑧𝑦)))
61, 5rexbida 3029 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑧𝐵 ↔ ∃𝑥𝐴𝑦(𝑦 = 𝐵𝑧𝑦)))
7 rexcom4 3198 . . . . 5 (∃𝑥𝐴𝑦(𝑦 = 𝐵𝑧𝑦) ↔ ∃𝑦𝑥𝐴 (𝑦 = 𝐵𝑧𝑦))
86, 7syl6bb 275 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑧𝐵 ↔ ∃𝑦𝑥𝐴 (𝑦 = 𝐵𝑧𝑦)))
9 r19.41v 3070 . . . . . 6 (∃𝑥𝐴 (𝑦 = 𝐵𝑧𝑦) ↔ (∃𝑥𝐴 𝑦 = 𝐵𝑧𝑦))
109exbii 1764 . . . . 5 (∃𝑦𝑥𝐴 (𝑦 = 𝐵𝑧𝑦) ↔ ∃𝑦(∃𝑥𝐴 𝑦 = 𝐵𝑧𝑦))
11 exancom 1774 . . . . 5 (∃𝑦(∃𝑥𝐴 𝑦 = 𝐵𝑧𝑦) ↔ ∃𝑦(𝑧𝑦 ∧ ∃𝑥𝐴 𝑦 = 𝐵))
1210, 11bitri 263 . . . 4 (∃𝑦𝑥𝐴 (𝑦 = 𝐵𝑧𝑦) ↔ ∃𝑦(𝑧𝑦 ∧ ∃𝑥𝐴 𝑦 = 𝐵))
138, 12syl6bb 275 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑧𝐵 ↔ ∃𝑦(𝑧𝑦 ∧ ∃𝑥𝐴 𝑦 = 𝐵)))
14 eliun 4460 . . 3 (𝑧 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑧𝐵)
15 eluniab 4383 . . 3 (𝑧 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑦(𝑧𝑦 ∧ ∃𝑥𝐴 𝑦 = 𝐵))
1613, 14, 153bitr4g 302 . 2 (∀𝑥𝐴 𝐵𝐶 → (𝑧 𝑥𝐴 𝐵𝑧 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}))
1716eqrdv 2608 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596  ∀wral 2896  ∃wrex 2897  ∪ cuni 4372  ∪ ciun 4455 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-uni 4373  df-iun 4457 This theorem is referenced by:  dfiun2  4490  dfiun3g  5299  iunexg  7035  uniqs  7694  ac6num  9184  iunopn  20528  pnrmopn  20957  cncmp  21005  ptcmplem3  21668  iunmbl  23128  voliun  23129  sigaclcuni  29508  sigaclcu2  29510  sigaclci  29522  measvunilem  29602  meascnbl  29609  carsgclctunlem3  29709
 Copyright terms: Public domain W3C validator