Theorem ssin 2232

Description: Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26.

Assertion

Ref	Expression
ssin	|- ((A (_ B /\ A (_ C) <-> A (_ (B i^i C))

Proof of Theorem ssin

Step	Hyp	Ref	Expression
1		ineq12 2212	. . . . 5 |- (((A i^i B) = A /\ (A i^i C) = A) -> ((A i^i B) i^i (A i^i C)) = (A i^i A))
2		inindi 2227	. . . . 5 |- (A i^i (B i^i C)) = ((A i^i B) i^i (A i^i C))
3	1, 2	syl5eq 1519	. . . 4 |- (((A i^i B) = A /\ (A i^i C) = A) -> (A i^i (B i^i C)) = (A i^i A))
4		inidm 2222	. . . 4 |- (A i^i A) = A
5	3, 4	syl6eq 1523	. . 3 |- (((A i^i B) = A /\ (A i^i C) = A) -> (A i^i (B i^i C)) = A)
6		df-ss 2053	. . . 4 |- (A (_ B <-> (A i^i B) = A)
7		df-ss 2053	. . . 4 |- (A (_ C <-> (A i^i C) = A)
8	6, 7	anbi12i 482	. . 3 |- ((A (_ B /\ A (_ C) <-> ((A i^i B) = A /\ (A i^i C) = A))
9		df-ss 2053	. . 3 |- (A (_ (B i^i C) <-> (A i^i (B i^i C)) = A)
10	5, 8, 9	3imtr4 219	. 2 |- ((A (_ B /\ A (_ C) -> A (_ (B i^i C))
11		inss1 2230	. . . 4 |- (B i^i C) (_ B
12		sstr2 2071	. . . 4 |- (A (_ (B i^i C) -> ((B i^i C) (_ B -> A (_ B))
13	11, 12	mpi 44	. . 3 |- (A (_ (B i^i C) -> A (_ B)
14		inss2 2231	. . . 4 |- (B i^i C) (_ C
15		sstr2 2071	. . . 4 |- (A (_ (B i^i C) -> ((B i^i C) (_ C -> A (_ C))
16	14, 15	mpi 44	. . 3 |- (A (_ (B i^i C) -> A (_ C)
17	13, 16	jca 288	. 2 |- (A (_ (B i^i C) -> (A (_ B /\ A (_ C))
18	10, 17	impbi 157	1 |- ((A (_ B /\ A (_ C) <-> A (_ (B i^i C))

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 956   i^i cin 2046   (_ wss 2047

This theorem is referenced by:  ssini 2233  nssinpss 2240  uneqin 2256  disjpss 2319  trin 2690  pwin 2825  fin 3651  zfregs 4647  tgvalt 7616  elcls 7704  innei 7736  chabs2t 9440  cmbr4 9544  pjin3 10122  mdbr2 10223  dmdbr2 10230  dmdbr5 10235  mdslle1 10244  mdslle2 10245  mdslj1 10246  mdslj2 10247  mdsl2 10249  mdsl2b 10250  mdslmd1lem1 10252  mdslmd1lem2 10253  mdslmd1 10256  mdslmd3 10259  hatomistic 10289  chrelat2 10292  cvexchlem 10295  mdsymlem1 10330  mdsymlem3 10332  mdsymlem5 10334  mdsymlem6 10335  dmdbr5at 10349  filintf 10569

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-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051  df-ss 2053

Copyright terms: Public domain