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 |
|
dfss2 |
|- ( A C_ ( _I o. B ) <-> A. x ( x e. A -> x e. ( _I o. B ) ) ) |
27 |
|
dfss2 |
|- ( 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 ) ) |