Metamath Proof Explorer


Theorem caovcl

Description: Convert an operation closure law to class notation. (Contributed by NM, 4-Aug-1995) (Revised by Mario Carneiro, 26-May-2014)

Ref Expression
Hypothesis caovcl.1 xSySxFyS
Assertion caovcl ASBSAFBS

Proof

Step Hyp Ref Expression
1 caovcl.1 xSySxFyS
2 tru
3 1 adantl xSySxFyS
4 3 caovclg ASBSAFBS
5 2 4 mpan ASBSAFBS