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

Theorem unss 3245
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 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)

Proof of Theorem unss
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dfss2 3081 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
2 19.26 1457 . . 3 (∀𝑥((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)) ↔ (∀𝑥(𝑥𝐴𝑥𝐶) ∧ ∀𝑥(𝑥𝐵𝑥𝐶)))
3 elun 3212 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43imbi1i 237 . . . . 5 ((𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) → 𝑥𝐶))
5 jaob 699 . . . . 5 (((𝑥𝐴𝑥𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)))
64, 5bitri 183 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)))
76albii 1446 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ∀𝑥((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)))
8 dfss2 3081 . . . 4 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
9 dfss2 3081 . . . 4 (𝐵𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
108, 9anbi12i 455 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (∀𝑥(𝑥𝐴𝑥𝐶) ∧ ∀𝑥(𝑥𝐵𝑥𝐶)))
112, 7, 103bitr4i 211 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ (𝐴𝐶𝐵𝐶))
121, 11bitr2i 184 1 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wo 697  wal 1329  wcel 1480  cun 3064  wss 3066
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-v 2683  df-un 3070  df-in 3072  df-ss 3079
This theorem is referenced by:  unssi  3246  unssd  3247  unssad  3248  unssbd  3249  uneqin  3322  undifss  3438  prss  3671  prssg  3672  tpss  3680  pwundifss  4202  ordsucss  4415  elnn  4514  eqrelrel  4635  xpsspw  4646  relun  4651  relcoi2  5064  dfer2  6423  fimaxre2  10991  uncld  12267  bdeqsuc  13064  exmid1stab  13180
  Copyright terms: Public domain W3C validator