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

Theorem dfiin2g 4524
 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 2912 . . . 4 (∀𝑥𝐴 𝑤𝐵 ↔ ∀𝑥(𝑥𝐴𝑤𝐵))
2 df-ral 2912 . . . . . 6 (∀𝑥𝐴 𝐵𝐶 ↔ ∀𝑥(𝑥𝐴𝐵𝐶))
3 eleq2 2687 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → (𝑤𝑧𝑤𝐵))
43biimprcd 240 . . . . . . . . . . . 12 (𝑤𝐵 → (𝑧 = 𝐵𝑤𝑧))
54alrimiv 1852 . . . . . . . . . . 11 (𝑤𝐵 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))
6 eqid 2621 . . . . . . . . . . . 12 𝐵 = 𝐵
7 eqeq1 2625 . . . . . . . . . . . . . 14 (𝑧 = 𝐵 → (𝑧 = 𝐵𝐵 = 𝐵))
87, 3imbi12d 334 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → ((𝑧 = 𝐵𝑤𝑧) ↔ (𝐵 = 𝐵𝑤𝐵)))
98spcgv 3282 . . . . . . . . . . . 12 (𝐵𝐶 → (∀𝑧(𝑧 = 𝐵𝑤𝑧) → (𝐵 = 𝐵𝑤𝐵)))
106, 9mpii 46 . . . . . . . . . . 11 (𝐵𝐶 → (∀𝑧(𝑧 = 𝐵𝑤𝑧) → 𝑤𝐵))
115, 10impbid2 216 . . . . . . . . . 10 (𝐵𝐶 → (𝑤𝐵 ↔ ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
1211imim2i 16 . . . . . . . . 9 ((𝑥𝐴𝐵𝐶) → (𝑥𝐴 → (𝑤𝐵 ↔ ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1312pm5.74d 262 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → ((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1413alimi 1736 . . . . . . 7 (∀𝑥(𝑥𝐴𝐵𝐶) → ∀𝑥((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
15 albi 1743 . . . . . . 7 (∀𝑥((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))) → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1614, 15syl 17 . . . . . 6 (∀𝑥(𝑥𝐴𝐵𝐶) → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
172, 16sylbi 207 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
18 df-ral 2912 . . . . . . . 8 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
1918albii 1744 . . . . . . 7 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑧𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
20 alcom 2034 . . . . . . 7 (∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑧𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
2119, 20bitr4i 267 . . . . . 6 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
22 r19.23v 3017 . . . . . . . 8 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ (∃𝑥𝐴 𝑧 = 𝐵𝑤𝑧))
23 vex 3192 . . . . . . . . . 10 𝑧 ∈ V
24 eqeq1 2625 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦 = 𝐵𝑧 = 𝐵))
2524rexbidv 3046 . . . . . . . . . 10 (𝑦 = 𝑧 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥𝐴 𝑧 = 𝐵))
2623, 25elab 3337 . . . . . . . . 9 (𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑥𝐴 𝑧 = 𝐵)
2726imbi1i 339 . . . . . . . 8 ((𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧) ↔ (∃𝑥𝐴 𝑧 = 𝐵𝑤𝑧))
2822, 27bitr4i 267 . . . . . . 7 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ (𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
2928albii 1744 . . . . . 6 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
30 19.21v 1865 . . . . . . 7 (∀𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
3130albii 1744 . . . . . 6 (∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
3221, 29, 313bitr3ri 291 . . . . 5 (∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
3317, 32syl6bb 276 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)))
341, 33syl5bb 272 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥𝐴 𝑤𝐵 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)))
3534abbidv 2738 . 2 (∀𝑥𝐴 𝐵𝐶 → {𝑤 ∣ ∀𝑥𝐴 𝑤𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)})
36 df-iin 4493 . 2 𝑥𝐴 𝐵 = {𝑤 ∣ ∀𝑥𝐴 𝑤𝐵}
37 df-int 4446 . 2 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)}
3835, 36, 373eqtr4g 2680 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1478   = wceq 1480   ∈ wcel 1987  {cab 2607  ∀wral 2907  ∃wrex 2908  ∩ cint 4445  ∩ ciin 4491 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-v 3191  df-int 4446  df-iin 4493 This theorem is referenced by:  dfiin2  4526  iinexg  4789  dfiin3g  5344  iinfi  8274  mreiincl  16184  iinopn  20635  clsval2  20773  alexsublem  21767
 Copyright terms: Public domain W3C validator