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

Theorem unss 3749
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 3557 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
2 19.26 1786 . . 3 (∀𝑥((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)) ↔ (∀𝑥(𝑥𝐴𝑥𝐶) ∧ ∀𝑥(𝑥𝐵𝑥𝐶)))
3 elun 3715 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
43imbi1i 338 . . . . 5 ((𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐵) → 𝑥𝐶))
5 jaob 818 . . . . 5 (((𝑥𝐴𝑥𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)))
64, 5bitri 263 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)))
76albii 1737 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ∀𝑥((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)))
8 dfss2 3557 . . . 4 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
9 dfss2 3557 . . . 4 (𝐵𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
108, 9anbi12i 729 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (∀𝑥(𝑥𝐴𝑥𝐶) ∧ ∀𝑥(𝑥𝐵𝑥𝐶)))
112, 7, 103bitr4i 291 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ (𝐴𝐶𝐵𝐶))
121, 11bitr2i 264 1 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wo 382  wa 383  wal 1473  wcel 1977  cun 3538  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554
This theorem is referenced by:  unssi  3750  unssd  3751  unssad  3752  unssbd  3753  nsspssun  3819  uneqin  3837  uneqdifeqOLD  4010  prssg  4290  prssOLD  4292  ssunsn2  4299  tpss  4308  iunopeqop  4906  pwundif  4945  eqrelrel  5144  xpsspw  5156  relun  5158  relcoi2  5580  fnsuppres  7209  wfrlem15  7316  dfer2  7630  isinf  8058  fiin  8211  trcl  8487  supxrun  12018  trclun  13603  isumltss  14419  rpnnen2lem12  14793  lcmfunsnlem  15192  lcmfun  15196  coprmprod  15213  coprmproddvdslem  15214  lubun  16946  isipodrs  16984  fpwipodrs  16987  ipodrsima  16988  aspval2  19168  unocv  19843  uncld  20655  restntr  20796  cmpcld  21015  uncmp  21016  ufprim  21523  tsmsfbas  21741  ovolctb2  23067  ovolun  23074  unmbl  23112  plyun0  23757  sshjcl  27598  sshjval2  27654  shlub  27657  ssjo  27690  spanuni  27787  dfon2lem3  30934  dfon2lem7  30938  clsun  31493  lindsenlbs  32574  mblfinlem3  32618  ismblfin  32620  paddssat  34118  pclunN  34202  paddunN  34231  poldmj1N  34232  pclfinclN  34254  lsmfgcl  36662  ssuncl  36894  sssymdifcl  36896  undmrnresiss  36929  mptrcllem  36939  cnvrcl0  36951  dfrtrcl5  36955  brtrclfv2  37038  unhe1  37099  dffrege76  37253  uneqsn  37341  clsk1indlem3  37361  setrec1lem4  42236  elpglem2  42254
  Copyright terms: Public domain W3C validator