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

Theorem unss 3090
 Description: The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.)
Assertion
Ref Expression
unss ((A𝐶 B𝐶) ↔ (AB) ⊆ 𝐶)

Proof of Theorem unss
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 dfss2 2907 . 2 ((AB) ⊆ 𝐶x(x (AB) → x 𝐶))
2 19.26 1346 . . 3 (x((x Ax 𝐶) (x Bx 𝐶)) ↔ (x(x Ax 𝐶) x(x Bx 𝐶)))
3 elun 3057 . . . . . 6 (x (AB) ↔ (x A x B))
43imbi1i 227 . . . . 5 ((x (AB) → x 𝐶) ↔ ((x A x B) → x 𝐶))
5 jaob 618 . . . . 5 (((x A x B) → x 𝐶) ↔ ((x Ax 𝐶) (x Bx 𝐶)))
64, 5bitri 173 . . . 4 ((x (AB) → x 𝐶) ↔ ((x Ax 𝐶) (x Bx 𝐶)))
76albii 1335 . . 3 (x(x (AB) → x 𝐶) ↔ x((x Ax 𝐶) (x Bx 𝐶)))
8 dfss2 2907 . . . 4 (A𝐶x(x Ax 𝐶))
9 dfss2 2907 . . . 4 (B𝐶x(x Bx 𝐶))
108, 9anbi12i 436 . . 3 ((A𝐶 B𝐶) ↔ (x(x Ax 𝐶) x(x Bx 𝐶)))
112, 7, 103bitr4i 201 . 2 (x(x (AB) → x 𝐶) ↔ (A𝐶 B𝐶))
121, 11bitr2i 174 1 ((A𝐶 B𝐶) ↔ (AB) ⊆ 𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 616  ∀wal 1224   ∈ wcel 1370   ∪ cun 2888   ⊆ wss 2890 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000 This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-un 2895  df-in 2897  df-ss 2904 This theorem is referenced by:  unssi  3091  unssd  3092  unssad  3093  unssbd  3094  nsspssun  3143  uneqin  3161  undifss  3276  prss  3490  prssg  3491  tpss  3499  pwundifss  3992  ordsucss  4176  elnn  4251  eqrelrel  4364  xpsspw  4373  relun  4377  relcoi2  4771  dfer2  6014  bdeqsuc  7327
 Copyright terms: Public domain W3C validator