Theorem seqomlem0

Description: Lemma for seqom . Change bound variables. (Contributed by Stefan O'Rear, 1-Nov-2014)

	Ref	Expression
Assertion	seqomlem0	|- rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) = rec ( ( c e. _om , d e. _V |-> <. suc c , ( c F d ) >. ) , <. (/) , ( _I ` I ) >. )

Proof

Step	Hyp	Ref	Expression
1		suceq	|- ( a = c -> suc a = suc c )
2		oveq1	|- ( a = c -> ( a F b ) = ( c F b ) )
3	1 2	opeq12d	|- ( a = c -> <. suc a , ( a F b ) >. = <. suc c , ( c F b ) >. )
4		oveq2	|- ( b = d -> ( c F b ) = ( c F d ) )
5	4	opeq2d	|- ( b = d -> <. suc c , ( c F b ) >. = <. suc c , ( c F d ) >. )
6	3 5	cbvmpov	|- ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) = ( c e. _om , d e. _V |-> <. suc c , ( c F d ) >. )
7		rdgeq1	|- ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) = ( c e. _om , d e. _V |-> <. suc c , ( c F d ) >. ) -> rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) = rec ( ( c e. _om , d e. _V |-> <. suc c , ( c F d ) >. ) , <. (/) , ( _I ` I ) >. ) )
8	6 7	ax-mp	|- rec ( ( a e. _om , b e. _V |-> <. suc a , ( a F b ) >. ) , <. (/) , ( _I ` I ) >. ) = rec ( ( c e. _om , d e. _V |-> <. suc c , ( c F d ) >. ) , <. (/) , ( _I ` I ) >. )