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

Theorem caovclg 6054
 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:   ,,   ,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hint:   ()

Proof of Theorem caovclg
StepHypRef Expression
1 caovclg.1 . . 3
21ralrimivva 2669 . 2
3 oveq1 5907 . . . 4
43eleq1d 2382 . . 3
5 oveq2 5908 . . . 4
65eleq1d 2382 . . 3
74, 6rspc2v 2924 . 2
82, 7mpan9 455 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   wceq 1633   wcel 1701  wral 2577  (class class class)co 5900 This theorem is referenced by:  caovcld  6055  caovcl  6056  grprinvd  6101  seqcl2  11111  seqcaopr  11130  ercpbl  13500  imasmnd2  14458  imasgrp2  14659  gsumzaddlem  15252  imasrng  15451  divsrhm  16038  mplind  16292  plymullem  19651  gsumpropd2lem  23357  esumpcvgval  23644 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903
 Copyright terms: Public domain W3C validator