Theorem caovcan

Description: Convert an operation cancellation law to class notation. (Contributed by NM, 20-Aug-1995)

	Ref	Expression
Hypotheses	caovcan.1	|- C e. _V
	caovcan.2	|- ( ( x e. S /\ y e. S ) -> ( ( x F y ) = ( x F z ) -> y = z ) )
Assertion	caovcan	|- ( ( A e. S /\ B e. S ) -> ( ( A F B ) = ( A F C ) -> B = C ) )

Proof

Step	Hyp	Ref	Expression
1		caovcan.1	|- C e. _V
2		caovcan.2	|- ( ( x e. S /\ y e. S ) -> ( ( x F y ) = ( x F z ) -> y = z ) )
3		oveq1	|- ( x = A -> ( x F y ) = ( A F y ) )
4		oveq1	|- ( x = A -> ( x F C ) = ( A F C ) )
5	3 4	eqeq12d	|- ( x = A -> ( ( x F y ) = ( x F C ) <-> ( A F y ) = ( A F C ) ) )
6	5	imbi1d	|- ( x = A -> ( ( ( x F y ) = ( x F C ) -> y = C ) <-> ( ( A F y ) = ( A F C ) -> y = C ) ) )
7		oveq2	|- ( y = B -> ( A F y ) = ( A F B ) )
8	7	eqeq1d	|- ( y = B -> ( ( A F y ) = ( A F C ) <-> ( A F B ) = ( A F C ) ) )
9		eqeq1	|- ( y = B -> ( y = C <-> B = C ) )
10	8 9	imbi12d	|- ( y = B -> ( ( ( A F y ) = ( A F C ) -> y = C ) <-> ( ( A F B ) = ( A F C ) -> B = C ) ) )
11		oveq2	|- ( z = C -> ( x F z ) = ( x F C ) )
12	11	eqeq2d	|- ( z = C -> ( ( x F y ) = ( x F z ) <-> ( x F y ) = ( x F C ) ) )
13		eqeq2	|- ( z = C -> ( y = z <-> y = C ) )
14	12 13	imbi12d	|- ( z = C -> ( ( ( x F y ) = ( x F z ) -> y = z ) <-> ( ( x F y ) = ( x F C ) -> y = C ) ) )
15	14	imbi2d	|- ( z = C -> ( ( ( x e. S /\ y e. S ) -> ( ( x F y ) = ( x F z ) -> y = z ) ) <-> ( ( x e. S /\ y e. S ) -> ( ( x F y ) = ( x F C ) -> y = C ) ) ) )
16	1 15 2	vtocl	|- ( ( x e. S /\ y e. S ) -> ( ( x F y ) = ( x F C ) -> y = C ) )
17	6 10 16	vtocl2ga	|- ( ( A e. S /\ B e. S ) -> ( ( A F B ) = ( A F C ) -> B = C ) )