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

Theorem dfiun2g 4660
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 3043 . . . . . 6 𝑥𝑥𝐴 𝐵𝐶
2 rsp 3031 . . . . . . . 8 (∀𝑥𝐴 𝐵𝐶 → (𝑥𝐴𝐵𝐶))
3 clel3g 3445 . . . . . . . 8 (𝐵𝐶 → (𝑧𝐵 ↔ ∃𝑦(𝑦 = 𝐵𝑧𝑦)))
42, 3syl6 35 . . . . . . 7 (∀𝑥𝐴 𝐵𝐶 → (𝑥𝐴 → (𝑧𝐵 ↔ ∃𝑦(𝑦 = 𝐵𝑧𝑦))))
54imp 444 . . . . . 6 ((∀𝑥𝐴 𝐵𝐶𝑥𝐴) → (𝑧𝐵 ↔ ∃𝑦(𝑦 = 𝐵𝑧𝑦)))
61, 5rexbida 3149 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑧𝐵 ↔ ∃𝑥𝐴𝑦(𝑦 = 𝐵𝑧𝑦)))
7 rexcom4 3329 . . . . 5 (∃𝑥𝐴𝑦(𝑦 = 𝐵𝑧𝑦) ↔ ∃𝑦𝑥𝐴 (𝑦 = 𝐵𝑧𝑦))
86, 7syl6bb 276 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑧𝐵 ↔ ∃𝑦𝑥𝐴 (𝑦 = 𝐵𝑧𝑦)))
9 r19.41v 3191 . . . . . 6 (∃𝑥𝐴 (𝑦 = 𝐵𝑧𝑦) ↔ (∃𝑥𝐴 𝑦 = 𝐵𝑧𝑦))
109exbii 1887 . . . . 5 (∃𝑦𝑥𝐴 (𝑦 = 𝐵𝑧𝑦) ↔ ∃𝑦(∃𝑥𝐴 𝑦 = 𝐵𝑧𝑦))
11 exancom 1900 . . . . 5 (∃𝑦(∃𝑥𝐴 𝑦 = 𝐵𝑧𝑦) ↔ ∃𝑦(𝑧𝑦 ∧ ∃𝑥𝐴 𝑦 = 𝐵))
1210, 11bitri 264 . . . 4 (∃𝑦𝑥𝐴 (𝑦 = 𝐵𝑧𝑦) ↔ ∃𝑦(𝑧𝑦 ∧ ∃𝑥𝐴 𝑦 = 𝐵))
138, 12syl6bb 276 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∃𝑥𝐴 𝑧𝐵 ↔ ∃𝑦(𝑧𝑦 ∧ ∃𝑥𝐴 𝑦 = 𝐵)))
14 eliun 4632 . . 3 (𝑧 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑧𝐵)
15 eluniab 4555 . . 3 (𝑧 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑦(𝑧𝑦 ∧ ∃𝑥𝐴 𝑦 = 𝐵))
1613, 14, 153bitr4g 303 . 2 (∀𝑥𝐴 𝐵𝐶 → (𝑧 𝑥𝐴 𝐵𝑧 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵}))
1716eqrdv 2722 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1596  wex 1817  wcel 2103  {cab 2710  wral 3014  wrex 3015   cuni 4544   ciun 4628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-v 3306  df-uni 4545  df-iun 4630
This theorem is referenced by:  dfiun2  4662  dfiun3g  5485  abnexg  7081  iunexg  7260  uniqs  7925  ac6num  9414  iunopn  20826  pnrmopn  21270  cncmp  21318  ptcmplem3  21980  iunmbl  23442  voliun  23443  sigaclcuni  30411  sigaclcu2  30413  sigaclci  30425  measvunilem  30505  meascnbl  30512  carsgclctunlem3  30612  uniqsALTV  34344
  Copyright terms: Public domain W3C validator