Step |
Hyp |
Ref |
Expression |
1 |
|
eleq1 |
|- ( x = A -> ( x e. P. <-> A e. P. ) ) |
2 |
1
|
anbi1d |
|- ( x = A -> ( ( x e. P. /\ y e. P. ) <-> ( A e. P. /\ y e. P. ) ) ) |
3 |
|
psseq1 |
|- ( x = A -> ( x C. y <-> A C. y ) ) |
4 |
2 3
|
anbi12d |
|- ( x = A -> ( ( ( x e. P. /\ y e. P. ) /\ x C. y ) <-> ( ( A e. P. /\ y e. P. ) /\ A C. y ) ) ) |
5 |
|
eleq1 |
|- ( y = B -> ( y e. P. <-> B e. P. ) ) |
6 |
5
|
anbi2d |
|- ( y = B -> ( ( A e. P. /\ y e. P. ) <-> ( A e. P. /\ B e. P. ) ) ) |
7 |
|
psseq2 |
|- ( y = B -> ( A C. y <-> A C. B ) ) |
8 |
6 7
|
anbi12d |
|- ( y = B -> ( ( ( A e. P. /\ y e. P. ) /\ A C. y ) <-> ( ( A e. P. /\ B e. P. ) /\ A C. B ) ) ) |
9 |
|
df-ltp |
|- . | ( ( x e. P. /\ y e. P. ) /\ x C. y ) } |
10 |
4 8 9
|
brabg |
|- ( ( A e. P. /\ B e. P. ) -> ( A ( ( A e. P. /\ B e. P. ) /\ A C. B ) ) ) |
11 |
10
|
bianabs |
|- ( ( A e. P. /\ B e. P. ) -> ( A A C. B ) ) |