Metamath Proof Explorer


Theorem sscoid

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

Ref Expression
Assertion sscoid A I B Rel A A B

Proof

Step Hyp Ref Expression
1 relco Rel I B
2 relss A I B Rel I B Rel A
3 1 2 mpi A I B Rel A
4 elrel Rel A x A y z x = y z
5 vex y V
6 vex z V
7 5 6 brco y I B z 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 x y B x x I z x x = z y B x
11 breq2 x = z y B x y B z
12 11 equsexvw x x = z y B x y B z
13 7 10 12 3bitri y I B z y B z
14 13 a1i x = y z y I B z y B z
15 eleq1 x = y z x I B y z I B
16 df-br y I B z y z I B
17 15 16 bitr4di x = y z x I B y I B z
18 eleq1 x = y z x B y z B
19 df-br y B z y z B
20 18 19 bitr4di x = y z x B y B z
21 14 17 20 3bitr4d x = y z x I B x B
22 21 exlimivv y z x = y z x I B x B
23 4 22 syl Rel A x A x I B x B
24 23 pm5.74da Rel A x A x I B x A x B
25 24 albidv Rel A x x A x I B x x A x B
26 dfss2 A I B x x A x I B
27 dfss2 A B x x A x B
28 25 26 27 3bitr4g Rel A A I B A B
29 3 28 biadanii A I B Rel A A B