Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
Could not format ( ( o = .o. /\ m = M ) -> m = M ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> m = M ) with typecode |- |
2 |
|
oveq |
Could not format ( o = .o. -> ( x o y ) = ( x .o. y ) ) : No typesetting found for |- ( o = .o. -> ( x o y ) = ( x .o. y ) ) with typecode |- |
3 |
2
|
adantr |
Could not format ( ( o = .o. /\ m = M ) -> ( x o y ) = ( x .o. y ) ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> ( x o y ) = ( x .o. y ) ) with typecode |- |
4 |
3 1
|
eleq12d |
Could not format ( ( o = .o. /\ m = M ) -> ( ( x o y ) e. m <-> ( x .o. y ) e. M ) ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> ( ( x o y ) e. m <-> ( x .o. y ) e. M ) ) with typecode |- |
5 |
1 4
|
raleqbidv |
Could not format ( ( o = .o. /\ m = M ) -> ( A. y e. m ( x o y ) e. m <-> A. y e. M ( x .o. y ) e. M ) ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> ( A. y e. m ( x o y ) e. m <-> A. y e. M ( x .o. y ) e. M ) ) with typecode |- |
6 |
1 5
|
raleqbidv |
Could not format ( ( o = .o. /\ m = M ) -> ( A. x e. m A. y e. m ( x o y ) e. m <-> A. x e. M A. y e. M ( x .o. y ) e. M ) ) : No typesetting found for |- ( ( o = .o. /\ m = M ) -> ( A. x e. m A. y e. m ( x o y ) e. m <-> A. x e. M A. y e. M ( x .o. y ) e. M ) ) with typecode |- |
7 |
|
df-cllaw |
|
8 |
6 7
|
brabga |
Could not format ( ( .o. e. V /\ M e. W ) -> ( .o. clLaw M <-> A. x e. M A. y e. M ( x .o. y ) e. M ) ) : No typesetting found for |- ( ( .o. e. V /\ M e. W ) -> ( .o. clLaw M <-> A. x e. M A. y e. M ( x .o. y ) e. M ) ) with typecode |- |