Theorem unss 4159

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 3954	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1867	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4153	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1816	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		dfss2 3954	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		dfss2 3954	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 628	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 305	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 278	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1531   ∈ wcel 2110   ∪ cun 3933   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940  df-in 3942  df-ss 3951

This theorem is referenced by:  unssi  4160  unssd  4161  unssad  4162  unssbd  4163  nsspssun  4233  uneqin  4254  prssg  4745  ssunsn2  4753  tpss  4761  iunopeqop  5403  pwundifOLD  5451  eqrelrel  5664  xpsspw  5676  relun  5678  relcoi2  6122  pwuncl  7486  fnsuppres  7851  wfrlem15  7963  dfer2  8284  isinf  8725  trcl  9164  supxrun  12703  trclun  14368  isumltss  15197  rpnnen2lem12  15572  lcmfunsnlem  15979  lcmfun  15983  coprmprod  15999  coprmproddvdslem  16000  lubun  17727  isipodrs  17765  ipodrsima  17769  aspval2  20121  unocv  20818  uncld  21643  restntr  21784  cmpcld  22004  uncmp  22005  ufprim  22511  tsmsfbas  22730  ovolctb2  24087  ovolun  24094  unmbl  24132  plyun0  24781  sshjcl  29126  sshjval2  29182  shlub  29185  ssjo  29218  spanuni  29315  cntzun  30690  dfon2lem3  33025  dfon2lem7  33029  noextendseq  33169  noresle  33195  clsun  33671  lindsadd  34879  lindsenlbs  34881  mblfinlem3  34925  ismblfin  34927  paddssat  36944  pclunN  37028  paddunN  37057  poldmj1N  37058  pclfinclN  37080  lsmfgcl  39667  ssuncl  39922  sssymdifcl  39924  undmrnresiss  39957  mptrcllem  39966  cnvrcl0  39978  dfrtrcl5  39982  brtrclfv2  40065  unhe1  40124  dffrege76  40278  uneqsn  40366  mnurndlem1  40610  setrec1lem4  44787  elpglem2  44808