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

Theorem unss 4146
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 3939 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
2 19.26 1872 . . 3 (∀𝑥((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)) ↔ (∀𝑥(𝑥𝐴𝑥𝐶) ∧ ∀𝑥(𝑥𝐵𝑥𝐶)))
3 elunant 4140 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)))
43albii 1821 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ∀𝑥((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)))
5 dfss2 3939 . . . 4 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
6 dfss2 3939 . . . 4 (𝐵𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
75, 6anbi12i 629 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (∀𝑥(𝑥𝐴𝑥𝐶) ∧ ∀𝑥(𝑥𝐵𝑥𝐶)))
82, 4, 73bitr4i 306 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ (𝐴𝐶𝐵𝐶))
91, 8bitr2i 279 1 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1536  wcel 2115  cun 3917  wss 3919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-in 3926  df-ss 3936
This theorem is referenced by:  unssi  4147  unssd  4148  unssad  4149  unssbd  4150  nsspssun  4219  uneqin  4240  prssg  4736  ssunsn2  4744  tpss  4752  iunopeqop  5399  pwundifOLD  5445  eqrelrel  5658  xpsspw  5670  relun  5672  relcoi2  6117  pwuncl  7488  fnsuppres  7855  wfrlem15  7967  dfer2  8288  isinf  8730  trcl  9169  supxrun  12708  trclun  14376  isumltss  15205  rpnnen2lem12  15580  lcmfunsnlem  15985  lcmfun  15989  coprmprod  16005  coprmproddvdslem  16006  lubun  17735  isipodrs  17773  ipodrsima  17777  unocv  20378  aspval2  20593  uncld  21655  restntr  21796  cmpcld  22016  uncmp  22017  ufprim  22523  tsmsfbas  22742  ovolctb2  24105  ovolun  24112  unmbl  24150  plyun0  24803  sshjcl  29147  sshjval2  29203  shlub  29206  ssjo  29239  spanuni  29336  cntzun  30737  dfon2lem3  33115  dfon2lem7  33119  noextendseq  33259  noresle  33285  clsun  33761  lindsadd  35022  lindsenlbs  35024  mblfinlem3  35068  ismblfin  35070  paddssat  37082  pclunN  37166  paddunN  37195  poldmj1N  37196  pclfinclN  37218  lsmfgcl  39962  ssuncl  40213  sssymdifcl  40215  undmrnresiss  40248  mptrcllem  40257  cnvrcl0  40269  dfrtrcl5  40273  brtrclfv2  40372  unhe1  40431  dffrege76  40585  uneqsn  40673  mnurndlem1  40937  setrec1lem4  45173  elpglem2  45194
  Copyright terms: Public domain W3C validator