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

Theorem dfiin2g 4932
 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 3135 . . . 4 (∀𝑥𝐴 𝑤𝐵 ↔ ∀𝑥(𝑥𝐴𝑤𝐵))
2 df-ral 3135 . . . . . 6 (∀𝑥𝐴 𝐵𝐶 ↔ ∀𝑥(𝑥𝐴𝐵𝐶))
3 eleq2 2902 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → (𝑤𝑧𝑤𝐵))
43biimprcd 253 . . . . . . . . . . . 12 (𝑤𝐵 → (𝑧 = 𝐵𝑤𝑧))
54alrimiv 1928 . . . . . . . . . . 11 (𝑤𝐵 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))
6 eqid 2822 . . . . . . . . . . . 12 𝐵 = 𝐵
7 eqeq1 2826 . . . . . . . . . . . . . 14 (𝑧 = 𝐵 → (𝑧 = 𝐵𝐵 = 𝐵))
87, 3imbi12d 348 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → ((𝑧 = 𝐵𝑤𝑧) ↔ (𝐵 = 𝐵𝑤𝐵)))
98spcgv 3570 . . . . . . . . . . . 12 (𝐵𝐶 → (∀𝑧(𝑧 = 𝐵𝑤𝑧) → (𝐵 = 𝐵𝑤𝐵)))
106, 9mpii 46 . . . . . . . . . . 11 (𝐵𝐶 → (∀𝑧(𝑧 = 𝐵𝑤𝑧) → 𝑤𝐵))
115, 10impbid2 229 . . . . . . . . . 10 (𝐵𝐶 → (𝑤𝐵 ↔ ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
1211imim2i 16 . . . . . . . . 9 ((𝑥𝐴𝐵𝐶) → (𝑥𝐴 → (𝑤𝐵 ↔ ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1312pm5.74d 276 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → ((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1413alimi 1813 . . . . . . 7 (∀𝑥(𝑥𝐴𝐵𝐶) → ∀𝑥((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
15 albi 1820 . . . . . . 7 (∀𝑥((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))) → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1614, 15syl 17 . . . . . 6 (∀𝑥(𝑥𝐴𝐵𝐶) → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
172, 16sylbi 220 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
18 df-ral 3135 . . . . . . . 8 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
1918albii 1821 . . . . . . 7 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑧𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
20 alcom 2163 . . . . . . 7 (∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑧𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
2119, 20bitr4i 281 . . . . . 6 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
22 r19.23v 3265 . . . . . . . 8 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ (∃𝑥𝐴 𝑧 = 𝐵𝑤𝑧))
23 vex 3472 . . . . . . . . . 10 𝑧 ∈ V
24 eqeq1 2826 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦 = 𝐵𝑧 = 𝐵))
2524rexbidv 3283 . . . . . . . . . 10 (𝑦 = 𝑧 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥𝐴 𝑧 = 𝐵))
2623, 25elab 3642 . . . . . . . . 9 (𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑥𝐴 𝑧 = 𝐵)
2726imbi1i 353 . . . . . . . 8 ((𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧) ↔ (∃𝑥𝐴 𝑧 = 𝐵𝑤𝑧))
2822, 27bitr4i 281 . . . . . . 7 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ (𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
2928albii 1821 . . . . . 6 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
30 19.21v 1940 . . . . . . 7 (∀𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
3130albii 1821 . . . . . 6 (∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
3221, 29, 313bitr3ri 305 . . . . 5 (∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
3317, 32syl6bb 290 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)))
341, 33syl5bb 286 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥𝐴 𝑤𝐵 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)))
3534abbidv 2886 . 2 (∀𝑥𝐴 𝐵𝐶 → {𝑤 ∣ ∀𝑥𝐴 𝑤𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)})
36 df-iin 4897 . 2 𝑥𝐴 𝐵 = {𝑤 ∣ ∀𝑥𝐴 𝑤𝐵}
37 df-int 4852 . 2 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)}
3835, 36, 373eqtr4g 2882 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   = wceq 1538   ∈ wcel 2114  {cab 2800  ∀wral 3130  ∃wrex 3131  ∩ cint 4851  ∩ ciin 4895 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-v 3471  df-int 4852  df-iin 4897 This theorem is referenced by:  dfiin2  4934  iinexg  5220  dfiin3g  5814  iinfi  8869  mreiincl  16858  iinopn  21505  clsval2  21653  alexsublem  22647
 Copyright terms: Public domain W3C validator