Theorem unss 2204

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 2173	. . . . 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 999	. 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 2058	. 2 |- ((A u. B) (_ C <-> A.x(x e. (A u. B) -> x e. C))
7		dfss2 2058	. . . 4 |- (A (_ C <-> A.x(x e. A -> x e. C))
8		dfss2 2058	. . . 4 |- (B (_ C <-> A.x(x e. B -> x e. C))
9	7, 8	anbi12i 482	. . 3 |- ((A (_ C /\ B (_ C) <-> (A.x(x e. A -> x e. C) /\ A.x(x e. B -> x e. C)))
10		19.26 1067	. . 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 954   e. wcel 958   u. cun 2045   (_ wss 2047

This theorem is referenced by:  unssi 2205  nsspssun 2241  uneqin 2256  eldifpw 2910  suceloni 3062  ordunel 3084  xpsspw 3257  relun 3261  dfer2 4262  abfii4OLD 4564  trcl 4645  supxrun 6085  infxpidmlem11 7562  subbasOLD 7644  uncld 7681  clslp 7748  dfchj2 9324  sshjclt 9327  shlub 9346  spanun 9467  infi1 10447  infi1OLD 10448  ficli 10472  ficliOLD 10473  infi 10578  infiOLD 10579  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem4 10591  rcfpfillem4OLD 10592

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-in 2051  df-ss 2053

Copyright terms: Public domain