ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfiin2g GIF version

Theorem dfiin2g 3737
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 2358 . . . 4 (∀𝑥𝐴 𝑤𝐵 ↔ ∀𝑥(𝑥𝐴𝑤𝐵))
2 df-ral 2358 . . . . . 6 (∀𝑥𝐴 𝐵𝐶 ↔ ∀𝑥(𝑥𝐴𝐵𝐶))
3 eleq2 2146 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → (𝑤𝑧𝑤𝐵))
43biimprcd 158 . . . . . . . . . . . 12 (𝑤𝐵 → (𝑧 = 𝐵𝑤𝑧))
54alrimiv 1797 . . . . . . . . . . 11 (𝑤𝐵 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))
6 eqid 2083 . . . . . . . . . . . 12 𝐵 = 𝐵
7 eqeq1 2089 . . . . . . . . . . . . . 14 (𝑧 = 𝐵 → (𝑧 = 𝐵𝐵 = 𝐵))
87, 3imbi12d 232 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → ((𝑧 = 𝐵𝑤𝑧) ↔ (𝐵 = 𝐵𝑤𝐵)))
98spcgv 2696 . . . . . . . . . . . 12 (𝐵𝐶 → (∀𝑧(𝑧 = 𝐵𝑤𝑧) → (𝐵 = 𝐵𝑤𝐵)))
106, 9mpii 43 . . . . . . . . . . 11 (𝐵𝐶 → (∀𝑧(𝑧 = 𝐵𝑤𝑧) → 𝑤𝐵))
115, 10impbid2 141 . . . . . . . . . 10 (𝐵𝐶 → (𝑤𝐵 ↔ ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
1211imim2i 12 . . . . . . . . 9 ((𝑥𝐴𝐵𝐶) → (𝑥𝐴 → (𝑤𝐵 ↔ ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1312pm5.74d 180 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → ((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1413alimi 1385 . . . . . . 7 (∀𝑥(𝑥𝐴𝐵𝐶) → ∀𝑥((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
15 albi 1398 . . . . . . 7 (∀𝑥((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))) → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1614, 15syl 14 . . . . . 6 (∀𝑥(𝑥𝐴𝐵𝐶) → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
172, 16sylbi 119 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
18 df-ral 2358 . . . . . . . 8 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
1918albii 1400 . . . . . . 7 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑧𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
20 alcom 1408 . . . . . . 7 (∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑧𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
2119, 20bitr4i 185 . . . . . 6 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
22 r19.23v 2475 . . . . . . . 8 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ (∃𝑥𝐴 𝑧 = 𝐵𝑤𝑧))
23 vex 2615 . . . . . . . . . 10 𝑧 ∈ V
24 eqeq1 2089 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦 = 𝐵𝑧 = 𝐵))
2524rexbidv 2375 . . . . . . . . . 10 (𝑦 = 𝑧 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥𝐴 𝑧 = 𝐵))
2623, 25elab 2748 . . . . . . . . 9 (𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑥𝐴 𝑧 = 𝐵)
2726imbi1i 236 . . . . . . . 8 ((𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧) ↔ (∃𝑥𝐴 𝑧 = 𝐵𝑤𝑧))
2822, 27bitr4i 185 . . . . . . 7 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ (𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
2928albii 1400 . . . . . 6 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
30 19.21v 1796 . . . . . . 7 (∀𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
3130albii 1400 . . . . . 6 (∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
3221, 29, 313bitr3ri 209 . . . . 5 (∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
3317, 32syl6bb 194 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)))
341, 33syl5bb 190 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥𝐴 𝑤𝐵 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)))
3534abbidv 2200 . 2 (∀𝑥𝐴 𝐵𝐶 → {𝑤 ∣ ∀𝑥𝐴 𝑤𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)})
36 df-iin 3707 . 2 𝑥𝐴 𝐵 = {𝑤 ∣ ∀𝑥𝐴 𝑤𝐵}
37 df-int 3663 . 2 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)}
3835, 36, 373eqtr4g 2140 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wal 1283   = wceq 1285  wcel 1434  {cab 2069  wral 2353  wrex 2354   cint 3662   ciin 3705
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-int 3663  df-iin 3707
This theorem is referenced by:  dfiin2  3739  iinexgm  3955  dfiin3g  4649  fniinfv  5307
  Copyright terms: Public domain W3C validator