Theorem unss 4188

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 3896	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1902	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4182	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1851	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3896	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3896	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 640	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 306	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 279	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   ∈ wcel 2144   ⊆ wss 3895   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151

This theorem is used by:  unssi  4189  unssd  4190  unssad  4191  unssbd  4192  nsspssun  4213  uneqin  4234  prssg  4774  ssunsn2  4782  tpss  4791  iunopeqop  5493  iunopeqopOLD  5494  eqrelrel  5772  xpsspw  5786  relun  5788  relcoi2  6280  pwuncl  7784  fnsuppres  8211  naddov3  8693  naddasslem1  8707  naddasslem2  8708  dfer2  8721  isinf  9259  trcl  9732  hfun  9921  setrec1lem4  9974  supxrun  13449  trclun  15172  isumltss  16022  rpnnen2lem12  16398  lcmfunsnlem  16821  lcmfun  16825  coprmprod  16841  coprmproddvdslem  16842  lubun  18694  isipodrs  18716  ipodrsima  18720  unocv  21991  lindsenlbs  22162  aspval2  22211  uncld  23364  restntr  23505  cmpcld  23725  uncmp  23726  ufprim  24233  tsmsfbas  24452  ovolctb2  25818  ovolun  25825  unmbl  25863  plyun0  26520  noextendseq  28029  noresle  28059  madebdayim  28279  sshjcl  31962  sshjval2  32018  shlub  32021  ssjo  32054  spanuni  32151  tpssg  33180  cntzun  33686  unitprodclb  33990  esplyind  34253  tz9.1regs  35858  dfon2lem3  36639  dfon2lem7  36643  clsun  37208  lindsadd  38629  mblfinlem3  38670  ismblfin  38672  paddssat  40964  pclunN  41048  paddunN  41077  poldmj1N  41078  pclfinclN  41100  lsmfgcl  44169  tfsconcatrnss  44445  ssuncl  44664  sssymdifcl  44666  undmrnresiss  44697  mptrcllem  44706  cnvrcl0  44718  dfrtrcl5  44722  brtrclfv2  44820  unhe1  44878  dffrege76  45032  uneqsn  45118  mnurndlem1  45358  gpgprismgr4cycllem8  49293  elpglem2  50973