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

Theorem dfiin2g 3717
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 2328 . . . 4 (∀𝑥𝐴 𝑤𝐵 ↔ ∀𝑥(𝑥𝐴𝑤𝐵))
2 df-ral 2328 . . . . . 6 (∀𝑥𝐴 𝐵𝐶 ↔ ∀𝑥(𝑥𝐴𝐵𝐶))
3 eleq2 2117 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → (𝑤𝑧𝑤𝐵))
43biimprcd 153 . . . . . . . . . . . 12 (𝑤𝐵 → (𝑧 = 𝐵𝑤𝑧))
54alrimiv 1770 . . . . . . . . . . 11 (𝑤𝐵 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))
6 eqid 2056 . . . . . . . . . . . 12 𝐵 = 𝐵
7 eqeq1 2062 . . . . . . . . . . . . . 14 (𝑧 = 𝐵 → (𝑧 = 𝐵𝐵 = 𝐵))
87, 3imbi12d 227 . . . . . . . . . . . . 13 (𝑧 = 𝐵 → ((𝑧 = 𝐵𝑤𝑧) ↔ (𝐵 = 𝐵𝑤𝐵)))
98spcgv 2657 . . . . . . . . . . . 12 (𝐵𝐶 → (∀𝑧(𝑧 = 𝐵𝑤𝑧) → (𝐵 = 𝐵𝑤𝐵)))
106, 9mpii 43 . . . . . . . . . . 11 (𝐵𝐶 → (∀𝑧(𝑧 = 𝐵𝑤𝑧) → 𝑤𝐵))
115, 10impbid2 135 . . . . . . . . . 10 (𝐵𝐶 → (𝑤𝐵 ↔ ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
1211imim2i 12 . . . . . . . . 9 ((𝑥𝐴𝐵𝐶) → (𝑥𝐴 → (𝑤𝐵 ↔ ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1312pm5.74d 175 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → ((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1413alimi 1360 . . . . . . 7 (∀𝑥(𝑥𝐴𝐵𝐶) → ∀𝑥((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
15 albi 1373 . . . . . . 7 (∀𝑥((𝑥𝐴𝑤𝐵) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))) → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
1614, 15syl 14 . . . . . 6 (∀𝑥(𝑥𝐴𝐵𝐶) → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
172, 16sylbi 118 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧))))
18 df-ral 2328 . . . . . . . 8 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
1918albii 1375 . . . . . . 7 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑧𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
20 alcom 1383 . . . . . . 7 (∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑧𝑥(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
2119, 20bitr4i 180 . . . . . 6 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)))
22 r19.23v 2442 . . . . . . . 8 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ (∃𝑥𝐴 𝑧 = 𝐵𝑤𝑧))
23 vex 2577 . . . . . . . . . 10 𝑧 ∈ V
24 eqeq1 2062 . . . . . . . . . . 11 (𝑦 = 𝑧 → (𝑦 = 𝐵𝑧 = 𝐵))
2524rexbidv 2344 . . . . . . . . . 10 (𝑦 = 𝑧 → (∃𝑥𝐴 𝑦 = 𝐵 ↔ ∃𝑥𝐴 𝑧 = 𝐵))
2623, 25elab 2709 . . . . . . . . 9 (𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} ↔ ∃𝑥𝐴 𝑧 = 𝐵)
2726imbi1i 231 . . . . . . . 8 ((𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧) ↔ (∃𝑥𝐴 𝑧 = 𝐵𝑤𝑧))
2822, 27bitr4i 180 . . . . . . 7 (∀𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ (𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
2928albii 1375 . . . . . 6 (∀𝑧𝑥𝐴 (𝑧 = 𝐵𝑤𝑧) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
30 19.21v 1769 . . . . . . 7 (∀𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ (𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
3130albii 1375 . . . . . 6 (∀𝑥𝑧(𝑥𝐴 → (𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)))
3221, 29, 313bitr3ri 204 . . . . 5 (∀𝑥(𝑥𝐴 → ∀𝑧(𝑧 = 𝐵𝑤𝑧)) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧))
3317, 32syl6bb 189 . . . 4 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥(𝑥𝐴𝑤𝐵) ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)))
341, 33syl5bb 185 . . 3 (∀𝑥𝐴 𝐵𝐶 → (∀𝑥𝐴 𝑤𝐵 ↔ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)))
3534abbidv 2171 . 2 (∀𝑥𝐴 𝐵𝐶 → {𝑤 ∣ ∀𝑥𝐴 𝑤𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)})
36 df-iin 3687 . 2 𝑥𝐴 𝐵 = {𝑤 ∣ ∀𝑥𝐴 𝑤𝐵}
37 df-int 3643 . 2 {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} = {𝑤 ∣ ∀𝑧(𝑧 ∈ {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵} → 𝑤𝑧)}
3835, 36, 373eqtr4g 2113 1 (∀𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102  wal 1257   = wceq 1259  wcel 1409  {cab 2042  wral 2323  wrex 2324   cint 3642   ciin 3685
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-v 2576  df-int 3643  df-iin 3687
This theorem is referenced by:  dfiin2  3719  iinexgm  3935  dfiin3g  4617  fniinfv  5258
  Copyright terms: Public domain W3C validator