Metamath Proof Explorer


Theorem caovcld

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 )

Proof

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 )