Description: Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 30-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | caovclg.1 | |- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x F y ) e. E ) |
|
caovcld.2 | |- ( ph -> A e. C ) |
||
caovcld.3 | |- ( ph -> B e. D ) |
||
Assertion | caovcld | |- ( ph -> ( A F B ) e. E ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | caovclg.1 | |- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x F y ) e. E ) |
|
2 | caovcld.2 | |- ( ph -> A e. C ) |
|
3 | caovcld.3 | |- ( ph -> B e. D ) |
|
4 | id | |- ( ph -> ph ) |
|
5 | 1 | caovclg | |- ( ( ph /\ ( A e. C /\ B e. D ) ) -> ( A F B ) e. E ) |
6 | 4 2 3 5 | syl12anc | |- ( ph -> ( A F B ) e. E ) |