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

Theorem unss 4190
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 df-ss 3968 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
2 19.26 1870 . . 3 (∀𝑥((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)) ↔ (∀𝑥(𝑥𝐴𝑥𝐶) ∧ ∀𝑥(𝑥𝐵𝑥𝐶)))
3 elunant 4184 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)))
43albii 1819 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ∀𝑥((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)))
5 df-ss 3968 . . . 4 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
6 df-ss 3968 . . . 4 (𝐵𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
75, 6anbi12i 628 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (∀𝑥(𝑥𝐴𝑥𝐶) ∧ ∀𝑥(𝑥𝐵𝑥𝐶)))
82, 4, 73bitr4i 303 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ (𝐴𝐶𝐵𝐶))
91, 8bitr2i 276 1 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1538  wcel 2108  cun 3949  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968
This theorem is referenced by:  unssi  4191  unssd  4192  unssad  4193  unssbd  4194  nsspssun  4268  uneqin  4289  prssg  4819  ssunsn2  4827  tpss  4837  iunopeqop  5526  eqrelrel  5807  xpsspw  5819  relun  5821  relcoi2  6297  pwuncl  7790  fnsuppres  8216  wfrlem15OLD  8363  naddov3  8718  naddasslem1  8732  naddasslem2  8733  dfer2  8746  isinf  9296  isinfOLD  9297  trcl  9768  supxrun  13358  trclun  15053  isumltss  15884  rpnnen2lem12  16261  lcmfunsnlem  16678  lcmfun  16682  coprmprod  16698  coprmproddvdslem  16699  lubun  18560  isipodrs  18582  ipodrsima  18586  unocv  21698  aspval2  21918  uncld  23049  restntr  23190  cmpcld  23410  uncmp  23411  ufprim  23917  tsmsfbas  24136  ovolctb2  25527  ovolun  25534  unmbl  25572  plyun0  26236  noextendseq  27712  noresle  27742  madebdayim  27926  sshjcl  31374  sshjval2  31430  shlub  31433  ssjo  31466  spanuni  31563  cntzun  33071  unitprodclb  33417  dfon2lem3  35786  dfon2lem7  35790  clsun  36329  lindsadd  37620  lindsenlbs  37622  mblfinlem3  37666  ismblfin  37668  paddssat  39816  pclunN  39900  paddunN  39929  poldmj1N  39930  pclfinclN  39952  lsmfgcl  43086  tfsconcatrnss  43363  ssuncl  43583  sssymdifcl  43585  undmrnresiss  43617  mptrcllem  43626  cnvrcl0  43638  dfrtrcl5  43642  brtrclfv2  43740  unhe1  43798  dffrege76  43952  uneqsn  44038  mnurndlem1  44300  setrec1lem4  49209  elpglem2  49231
  Copyright terms: Public domain W3C validator