Theorem unss 4126

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.

Step	Hyp	Ref	Expression
1		df-ss 3907	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1877	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4120	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1826	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3907	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3907	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 634	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 304	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 277	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545   ∈ wcel 2119   ∪ cun 3888   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907

This theorem is referenced by:  unssi  4127  unssd  4128  unssad  4129  unssbd  4130  nsspssun  4203  uneqin  4224  prssg  4757  ssunsn2  4765  tpss  4775  iunopeqop  5469  iunopeqopOLD  5470  eqrelrel  5747  xpsspw  5759  relun  5761  relcoi2  6235  pwuncl  7720  fnsuppres  8138  naddov3  8613  naddasslem1  8627  naddasslem2  8628  dfer2  8641  isinf  9172  trcl  9647  supxrun  13266  trclun  14974  isumltss  15811  rpnnen2lem12  16190  lcmfunsnlem  16608  lcmfun  16612  coprmprod  16628  coprmproddvdslem  16629  lubun  18479  isipodrs  18501  ipodrsima  18505  unocv  21662  aspval2  21880  uncld  23031  restntr  23172  cmpcld  23392  uncmp  23393  ufprim  23899  tsmsfbas  24118  ovolctb2  25484  ovolun  25491  unmbl  25529  plyun0  26187  noextendseq  27656  noresle  27686  madebdayim  27905  sshjcl  31451  sshjval2  31507  shlub  31510  ssjo  31543  spanuni  31640  tpssg  32632  cntzun  33167  unitprodclb  33479  esplyind  33766  tz9.1regs  35322  dfon2lem3  36018  dfon2lem7  36022  clsun  36563  lindsadd  37987  lindsenlbs  37989  mblfinlem3  38033  ismblfin  38035  paddssat  40313  pclunN  40397  paddunN  40426  poldmj1N  40427  pclfinclN  40449  lsmfgcl  43526  tfsconcatrnss  43802  ssuncl  44021  sssymdifcl  44023  undmrnresiss  44055  mptrcllem  44064  cnvrcl0  44076  dfrtrcl5  44080  brtrclfv2  44178  unhe1  44236  dffrege76  44390  uneqsn  44476  mnurndlem1  44732  gpgprismgr4cycllem8  48600  setrec1lem4  50187  elpglem2  50209