Theorem caovclg 6254

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

Hypothesis

Ref	Expression
caovclg.1	|- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x F y ) e. E )

Assertion

Ref	Expression
caovclg	|- ( ( ph /\ ( A e. C /\ B e. D ) ) -> ( A F B ) e. E )

Distinct variable groups:   x, y, A   y, B   x, C, y   x, D, y   x, E, y   ph, x, y   x, F, y

Allowed substitution hint:   B( x)

Proof of Theorem caovclg

Step	Hyp	Ref	Expression
1		caovclg.1	. . 3 |- ( ( ph /\ ( x e. C /\ y e. D ) ) -> ( x F y ) e. E )
2	1	ralrimivva 2806	. 2 |- ( ph -> A. x e. C A. y e. D ( x F y ) e. E )
3		oveq1 6097	. . . 4 |- ( x = A -> ( x F y ) = ( A F y ) )
4	3	eleq1d 2507	. . 3 |- ( x = A -> ( ( x F y ) e. E <-> ( A F y ) e. E ) )
5		oveq2 6098	. . . 4 |- ( y = B -> ( A F y ) = ( A F B ) )
6	5	eleq1d 2507	. . 3 |- ( y = B -> ( ( A F y ) e. E <-> ( A F B ) e. E ) )
7	4, 6	rspc2v 3076	. 2 |- ( ( A e. C /\ B e. D ) -> ( A. x e. C A. y e. D ( x F y ) e. E -> ( A F B ) e. E ) )
8	2, 7	mpan9 466	1 |- ( ( ph /\ ( A e. C /\ B e. D ) ) -> ( A F B ) e. E )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1364   e. wcel 1761   A.wral 2713  (class class class)co 6090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-iota 5378  df-fv 5423  df-ov 6093

This theorem is referenced by:  caovcld  6255  caovcl  6256  grprinvd  6301  seqcl2  11820  seqcaopr  11839  ercpbl  14483  imasmnd2  15454  imasgrp2  15663  gsumzaddlem  16401  gsumzaddlemOLD  16403  imasrng  16701  divsrhm  17297  mplind  17560  plymullem  21643  gsumpropd2lem  26177