Theorem unss 2194

Description: The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse.

Assertion

Ref	Expression
unss	|- ((A (_ C /\ B (_ C) <-> (A u. B) (_ C)

Proof of Theorem unss

Step	Hyp	Ref	Expression
1		elun 2163	. . . . 5 |- (x e. (A u. B) <-> (x e. A \/ x e. B))
2	1	imbi1i 186	. . . 4 |- ((x e. (A u. B) -> x e. C) <-> ((x e. A \/ x e. B) -> x e. C))
3		jaob 422	. . . 4 |- (((x e. A \/ x e. B) -> x e. C) <-> ((x e. A -> x e. C) /\ (x e. B -> x e. C)))
4	2, 3	bitr 173	. . 3 |- ((x e. (A u. B) -> x e. C) <-> ((x e. A -> x e. C) /\ (x e. B -> x e. C)))
5	4	albii 996	. 2 |- (A.x(x e. (A u. B) -> x e. C) <-> A.x((x e. A -> x e. C) /\ (x e. B -> x e. C)))
6		dfss2 2048	. 2 |- ((A u. B) (_ C <-> A.x(x e. (A u. B) -> x e. C))
7		dfss2 2048	. . . 4 |- (A (_ C <-> A.x(x e. A -> x e. C))
8		dfss2 2048	. . . 4 |- (B (_ C <-> A.x(x e. B -> x e. C))
9	7, 8	anbi12i 481	. . 3 |- ((A (_ C /\ B (_ C) <-> (A.x(x e. A -> x e. C) /\ A.x(x e. B -> x e. C)))
10		19.26 1063	. . 3 |- (A.x((x e. A -> x e. C) /\ (x e. B -> x e. C)) <-> (A.x(x e. A -> x e. C) /\ A.x(x e. B -> x e. C)))
11	9, 10	bitr4 176	. 2 |- ((A (_ C /\ B (_ C) <-> A.x((x e. A -> x e. C) /\ (x e. B -> x e. C)))
12	5, 6, 11	3bitr4r 184	1 |- ((A (_ C /\ B (_ C) <-> (A u. B) (_ C)

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223  A.wal 951   e. wcel 955   u. cun 2035   (_ wss 2037

This theorem is referenced by:  unssi 2195  nsspssun 2231  uneqin 2246  eldifpw 2900  suceloni 3052  ordunel 3074  xpsspw 3247  relun 3251  dfer2 4246  abfii4 4538  trcl 4617  supxrun 6032  infxpidmlem11 7505  subbas 7586  uncld 7623  clslp 7689  dfchj2 9239  sshjclt 9242  shlub 9261  spanun 9382  infi1 10347  ficli 10368  infi 10448  cnfilca 10451

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-in 2041  df-ss 2043

Copyright terms: Public domain