Theorem unss 4118

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		dfss2 3907	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1873	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4112	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1822	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		dfss2 3907	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		dfss2 3907	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 627	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 303	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 275	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   ∈ wcel 2106   ∪ cun 3885   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904

This theorem is referenced by:  unssi  4119  unssd  4120  unssad  4121  unssbd  4122  nsspssun  4191  uneqin  4212  prssg  4752  ssunsn2  4760  tpss  4768  iunopeqop  5435  pwundifOLD  5486  eqrelrel  5707  xpsspw  5719  relun  5721  relcoi2  6180  pwuncl  7620  fnsuppres  8007  wfrlem15OLD  8154  dfer2  8499  isinf  9036  trcl  9486  supxrun  13050  trclun  14725  isumltss  15560  rpnnen2lem12  15934  lcmfunsnlem  16346  lcmfun  16350  coprmprod  16366  coprmproddvdslem  16367  lubun  18233  isipodrs  18255  ipodrsima  18259  unocv  20885  aspval2  21102  uncld  22192  restntr  22333  cmpcld  22553  uncmp  22554  ufprim  23060  tsmsfbas  23279  ovolctb2  24656  ovolun  24663  unmbl  24701  plyun0  25358  sshjcl  29717  sshjval2  29773  shlub  29776  ssjo  29809  spanuni  29906  cntzun  31320  dfon2lem3  33761  dfon2lem7  33765  noextendseq  33870  noresle  33900  madebdayim  34070  clsun  34517  lindsadd  35770  lindsenlbs  35772  mblfinlem3  35816  ismblfin  35818  paddssat  37828  pclunN  37912  paddunN  37941  poldmj1N  37942  pclfinclN  37964  lsmfgcl  40899  ssuncl  41177  sssymdifcl  41179  undmrnresiss  41212  mptrcllem  41221  cnvrcl0  41233  dfrtrcl5  41237  brtrclfv2  41335  unhe1  41393  dffrege76  41547  uneqsn  41633  mnurndlem1  41899  setrec1lem4  46396  elpglem2  46417