Theorem sscoid

Description: A condition for subset and composition with identity. (Contributed by Scott Fenton, 13-Apr-2018)

	Ref	Expression
Assertion	sscoid	|- ( A C_ ( _I o. B ) <-> ( Rel A /\ A C_ B ) )

Proof

Step	Hyp	Ref	Expression
1		relco	|- Rel ( _I o. B )
2		relss	|- ( A C_ ( _I o. B ) -> ( Rel ( _I o. B ) -> Rel A ) )
3	1 2	mpi	|- ( A C_ ( _I o. B ) -> Rel A )
4		elrel	|- ( ( Rel A /\ x e. A ) -> E. y E. z x = <. y , z >. )
5		vex	|- y e. _V
6		vex	|- z e. _V
7	5 6	brco	|- ( y ( _I o. B ) z <-> E. x ( y B x /\ x _I z ) )
8	6	ideq	|- ( x _I z <-> x = z )
9	8	anbi1ci	|- ( ( y B x /\ x _I z ) <-> ( x = z /\ y B x ) )
10	9	exbii	|- ( E. x ( y B x /\ x _I z ) <-> E. x ( x = z /\ y B x ) )
11		breq2	|- ( x = z -> ( y B x <-> y B z ) )
12	11	equsexvw	|- ( E. x ( x = z /\ y B x ) <-> y B z )
13	7 10 12	3bitri	|- ( y ( _I o. B ) z <-> y B z )
14	13	a1i	|- ( x = <. y , z >. -> ( y ( _I o. B ) z <-> y B z ) )
15		eleq1	|- ( x = <. y , z >. -> ( x e. ( _I o. B ) <-> <. y , z >. e. ( _I o. B ) ) )
16		df-br	|- ( y ( _I o. B ) z <-> <. y , z >. e. ( _I o. B ) )
17	15 16	bitr4di	|- ( x = <. y , z >. -> ( x e. ( _I o. B ) <-> y ( _I o. B ) z ) )
18		eleq1	|- ( x = <. y , z >. -> ( x e. B <-> <. y , z >. e. B ) )
19		df-br	|- ( y B z <-> <. y , z >. e. B )
20	18 19	bitr4di	|- ( x = <. y , z >. -> ( x e. B <-> y B z ) )
21	14 17 20	3bitr4d	|- ( x = <. y , z >. -> ( x e. ( _I o. B ) <-> x e. B ) )
22	21	exlimivv	|- ( E. y E. z x = <. y , z >. -> ( x e. ( _I o. B ) <-> x e. B ) )
23	4 22	syl	|- ( ( Rel A /\ x e. A ) -> ( x e. ( _I o. B ) <-> x e. B ) )
24	23	pm5.74da	|- ( Rel A -> ( ( x e. A -> x e. ( _I o. B ) ) <-> ( x e. A -> x e. B ) ) )
25	24	albidv	|- ( Rel A -> ( A. x ( x e. A -> x e. ( _I o. B ) ) <-> A. x ( x e. A -> x e. B ) ) )
26		df-ss	|- ( A C_ ( _I o. B ) <-> A. x ( x e. A -> x e. ( _I o. B ) ) )
27		df-ss	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
28	25 26 27	3bitr4g	|- ( Rel A -> ( A C_ ( _I o. B ) <-> A C_ B ) )
29	3 28	biadanii	|- ( A C_ ( _I o. B ) <-> ( Rel A /\ A C_ B ) )