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

Theorem unss 4184
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 3963 . 2 ((𝐴𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶))
2 19.26 1865 . . 3 (∀𝑥((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)) ↔ (∀𝑥(𝑥𝐴𝑥𝐶) ∧ ∀𝑥(𝑥𝐵𝑥𝐶)))
3 elunant 4178 . . . 4 ((𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)))
43albii 1813 . . 3 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ ∀𝑥((𝑥𝐴𝑥𝐶) ∧ (𝑥𝐵𝑥𝐶)))
5 df-ss 3963 . . . 4 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
6 df-ss 3963 . . . 4 (𝐵𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
75, 6anbi12i 626 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (∀𝑥(𝑥𝐴𝑥𝐶) ∧ ∀𝑥(𝑥𝐵𝑥𝐶)))
82, 4, 73bitr4i 302 . 2 (∀𝑥(𝑥 ∈ (𝐴𝐵) → 𝑥𝐶) ↔ (𝐴𝐶𝐵𝐶))
91, 8bitr2i 275 1 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1531  wcel 2098  cun 3944  wss 3946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-un 3951  df-ss 3963
This theorem is referenced by:  unssi  4185  unssd  4186  unssad  4187  unssbd  4188  nsspssun  4258  uneqin  4279  prssg  4827  ssunsn2  4835  tpss  4843  iunopeqop  5526  eqrelrel  5802  xpsspw  5814  relun  5816  relcoi2  6287  pwuncl  7777  fnsuppres  8204  wfrlem15OLD  8352  naddov3  8709  naddasslem1  8723  naddasslem2  8724  dfer2  8734  isinf  9297  isinfOLD  9298  trcl  9767  supxrun  13344  trclun  15014  isumltss  15847  rpnnen2lem12  16222  lcmfunsnlem  16637  lcmfun  16641  coprmprod  16657  coprmproddvdslem  16658  lubun  18535  isipodrs  18557  ipodrsima  18561  unocv  21668  aspval2  21887  uncld  23028  restntr  23169  cmpcld  23389  uncmp  23390  ufprim  23896  tsmsfbas  24115  ovolctb2  25504  ovolun  25511  unmbl  25549  plyun0  26216  noextendseq  27689  noresle  27719  madebdayim  27903  sshjcl  31280  sshjval2  31336  shlub  31339  ssjo  31372  spanuni  31469  cntzun  32906  unitprodclb  33241  dfon2lem3  35557  dfon2lem7  35561  clsun  35988  lindsadd  37262  lindsenlbs  37264  mblfinlem3  37308  ismblfin  37310  paddssat  39461  pclunN  39545  paddunN  39574  poldmj1N  39575  pclfinclN  39597  lsmfgcl  42672  tfsconcatrnss  42953  ssuncl  43174  sssymdifcl  43176  undmrnresiss  43208  mptrcllem  43217  cnvrcl0  43229  dfrtrcl5  43233  brtrclfv2  43331  unhe1  43389  dffrege76  43543  uneqsn  43629  mnurndlem1  43892  setrec1lem4  48373  elpglem2  48395
  Copyright terms: Public domain W3C validator