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.

Step	Hyp	Ref	Expression
1		df-ss 3963	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1865	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4178	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1813	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3963	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3963	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 626	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 302	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 275	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

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