MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  caovclg Unicode version

Theorem caovclg 6467
Description: Convert an operation closure law to class notation. (Contributed by Mario Carneiro, 26-May-2014.)
Hypothesis
Ref Expression
caovclg.1
Assertion
Ref Expression
caovclg
Distinct variable groups:   , ,   ,   , ,   , ,   , ,   , ,   , ,

Proof of Theorem caovclg
StepHypRef Expression
1 caovclg.1 . . 3
21ralrimivva 2878 . 2
3 oveq1 6303 . . . 4
43eleq1d 2526 . . 3
5 oveq2 6304 . . . 4
65eleq1d 2526 . . 3
74, 6rspc2v 3219 . 2
82, 7mpan9 469 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807  (class class class)co 6296
This theorem is referenced by:  caovcld  6468  caovcl  6469  grprinvd  6514  seqcl2  12125  seqcaopr  12144  ercpbl  14946  gsumpropd2lem  15900  imasmnd2  15957  imasgrp2  16185  gsumzaddlem  16934  gsumzaddlemOLD  16936  imasring  17268  qusrhm  17885  mplind  18167  plymullem  22613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299
  Copyright terms: Public domain W3C validator