Theorem unss 4142

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 3921	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1889	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4136	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1838	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3921	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3921	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 637	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 305	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 278	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557   ∈ wcel 2141   ∪ cun 3902   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921

This theorem is referenced by:  unssi  4143  unssd  4144  unssad  4145  unssbd  4146  nsspssun  4220  uneqin  4241  prssg  4776  ssunsn2  4784  tpss  4794  iunopeqop  5489  iunopeqopOLD  5490  eqrelrel  5767  xpsspw  5780  relun  5782  relcoi2  6260  pwuncl  7749  fnsuppres  8166  naddov3  8646  naddasslem1  8660  naddasslem2  8661  dfer2  8674  isinf  9205  trcl  9680  supxrun  13316  trclun  15024  isumltss  15861  rpnnen2lem12  16240  lcmfunsnlem  16658  lcmfun  16662  coprmprod  16678  coprmproddvdslem  16679  lubun  18530  isipodrs  18552  ipodrsima  18556  unocv  21712  aspval2  21930  uncld  23081  restntr  23222  cmpcld  23442  uncmp  23443  ufprim  23949  tsmsfbas  24168  ovolctb2  25534  ovolun  25541  unmbl  25579  plyun0  26237  noextendseq  27708  noresle  27738  madebdayim  27958  sshjcl  31504  sshjval2  31560  shlub  31563  ssjo  31596  spanuni  31693  tpssg  32685  cntzun  33220  unitprodclb  33536  esplyind  33833  tz9.1regs  35394  dfon2lem3  36097  dfon2lem7  36101  clsun  36652  lindsadd  38076  lindsenlbs  38078  mblfinlem3  38122  ismblfin  38124  paddssat  40402  pclunN  40486  paddunN  40515  poldmj1N  40516  pclfinclN  40538  lsmfgcl  43615  tfsconcatrnss  43891  ssuncl  44110  sssymdifcl  44112  undmrnresiss  44144  mptrcllem  44153  cnvrcl0  44165  dfrtrcl5  44169  brtrclfv2  44267  unhe1  44325  dffrege76  44479  uneqsn  44565  mnurndlem1  44821  gpgprismgr4cycllem8  48688  setrec1lem4  50275  elpglem2  50297