Theorem ssin 2228

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 2208	. . . . 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 2223	. . . . 5 |- (A i^i (B i^i C)) = ((A i^i B) i^i (A i^i C))
3	1, 2	syl5eq 1516	. . . 4 |- (((A i^i B) = A /\ (A i^i C) = A) -> (A i^i (B i^i C)) = (A i^i A))
4		inidm 2218	. . . 4 |- (A i^i A) = A
5	3, 4	syl6eq 1520	. . 3 |- (((A i^i B) = A /\ (A i^i C) = A) -> (A i^i (B i^i C)) = A)
6		df-ss 2049	. . . 4 |- (A (_ B <-> (A i^i B) = A)
7		df-ss 2049	. . . 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 2049	. . 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 2226	. . . 4 |- (B i^i C) (_ B
12		sstr2 2067	. . . 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 2227	. . . 4 |- (B i^i C) (_ C
15		sstr2 2067	. . . 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 954   i^i cin 2042   (_ wss 2043

This theorem is referenced by:  ssini 2229  nssinpss 2236  uneqin 2252  disjpss 2315  trin 2685  pwin 2820  fin 3642  zfregs 4627  tgvalt 7566  elcls 7654  innei 7686  chabs2t 9378  cmbr4 9484  pjin3 10060  mdbr2 10161  dmdbr2 10168  mdslle1 10181  mdslle2 10182  mdslj1 10183  mdslj2 10184  mdsl2 10186  mdsl2b 10187  mdslmd1lem1 10189  mdslmd1lem2 10190  mdslmd1 10193  mdslmd3 10196  hatomistic 10226  chrelat2 10229  cvexchlem 10232  mdsymlem1 10267  mdsymlem3 10269  mdsymlem5 10271  mdsymlem6 10272  dmdbr5at 10284  filintf 10479

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-ss 2049

Copyright terms: Public domain