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

Theorem dfiin2g 4961
Description: Alternate definition of indexed intersection when 𝐵 is a set. (Contributed by Jeff Hankins, 27-Aug-2009.)
Assertion
Ref Expression
dfiin2g (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥,𝑦)

Proof of Theorem dfiin2g
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ral 3069 . . . 4 (∀𝑥𝐴 𝑤𝐵 ↔ ∀𝑥(𝑥𝐴𝑤𝐵))
2 df-ral 3069 . . . . . 6 (∀𝑥𝐴 𝐵𝐶 ↔ ∀𝑥(𝑥𝐴𝐵𝐶))
3 eleq2 2827 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → (𝑤𝑧𝑤𝐵))
43biimprcd 249 . . . . . . . . . . . 12 (𝑤𝐵 → (𝑧 = 𝐵𝑤𝑧))
54alrimiv 1930 . . . . . . . . . . 11 (𝑤𝐵 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))
6 eqid 2738 . . . . . . . . . . . 12 𝐵 = 𝐵
7 eqeq1 2742 . . . . . . . . . . . . . 14 (𝑧 = 𝐵 → (𝑧 = 𝐵𝐵 = 𝐵))
87, 3imbi12d 345 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → ((𝑧 = 𝐵𝑤𝑧) ↔ (𝐵 = 𝐵𝑤𝐵)))
98spcgv 3532 . . . . . . . . . . . 12 (𝐵𝐶 → (∀𝑧(𝑧 = 𝐵𝑤𝑧) → (𝐵 = 𝐵𝑤𝐵)))
106, 9mpii 46 . . . . . . . . . . 11 (𝐵𝐶 → (∀𝑧(𝑧 = 𝐵𝑤𝑧) → 𝑤𝐵))
115, 10impbid2 225 . . . . . . . . . 10 (𝐵𝐶 → (𝑤𝐵 ↔ ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
1211imim2i 16 . . . . . . . . 9 ((𝑥𝐴𝐵𝐶) → (𝑥𝐴 → (𝑤𝐵 ↔ ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1312pm5.74d 272 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → ((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1413alimi 1814 . . . . . . 7 (∀𝑥(𝑥𝐴𝐵𝐶) → ∀𝑥((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
15 albi 1821 . . . . . . 7 (∀𝑥((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))) → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1614, 15syl 17 . . . . . 6 (∀𝑥(𝑥𝐴𝐵𝐶) → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
172, 16sylbi 216 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
18 df-ral 3069 . . . . . . . 8 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
1918albii 1822 . . . . . . 7 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑧𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
20 alcom 2156 . . . . . . 7 (∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑧𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
2119, 20bitr4i 277 . . . . . 6 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
22 r19.23v 3206 . . . . . . . 8 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ (∃𝑥𝐴 𝑧 = 𝐵𝑤𝑧))
23 vex 3433 . . . . . . . . . 10 𝑧 ∈ V
24 eqeq1 2742 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦 = 𝐵𝑧 = 𝐵))
2524rexbidv 3224 . . . . . . . . . 10 (𝑦 = 𝑧 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥𝐴 𝑧 = 𝐵))
2623, 25elab 3608 . . . . . . . . 9 (𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑥𝐴 𝑧 = 𝐵)
2726imbi1i 350 . . . . . . . 8 ((𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧) ↔ (∃𝑥𝐴 𝑧 = 𝐵𝑤𝑧))
2822, 27bitr4i 277 . . . . . . 7 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ (𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
2928albii 1822 . . . . . 6 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
30 19.21v 1942 . . . . . . 7 (∀𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
3130albii 1822 . . . . . 6 (∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
3221, 29, 313bitr3ri 302 . . . . 5 (∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
3317, 32bitrdi 287 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)))
341, 33bitrid 282 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥𝐴 𝑤𝐵 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)))
3534abbidv 2807 . 2 (∀𝑥𝐴 𝐵𝐶 → {𝑤 ∣ ∀𝑥𝐴 𝑤𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)})
36 df-iin 4927 . 2 𝑥𝐴 𝐵 = {𝑤 ∣ ∀𝑥𝐴 𝑤𝐵}
37 df-int 4880 . 2 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)}
3835, 36, 373eqtr4g 2803 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1537   = wceq 1539  wcel 2106  {cab 2715  wral 3064  wrex 3065   cint 4879   ciin 4925
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3431  df-int 4880  df-iin 4927
This theorem is referenced by:  dfiin2  4963  iinexg  5263  dfiin3g  5867  iinfi  9163  mreiincl  17315  iinopn  22061  clsval2  22211  alexsublem  23205
  Copyright terms: Public domain W3C validator