seqomlem0

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

		Ref	Expression
	Assertion	seqomlem0	$⊢ rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) = rec ((c \in ω, d \in V ⟼ ⟨suc c, c F d⟩), ⟨\emptyset, I (I)⟩)$

Step	Hyp	Ref	Expression
1		suceq	$⊢ a = c \to suc a = suc c$
2		oveq1	$⊢ a = c \to a F b = c F b$
3	1 2	opeq12d	$⊢ a = c \to ⟨suc a, a F b⟩ = ⟨suc c, c F b⟩$
4		oveq2	$⊢ b = d \to c F b = c F d$
5	4	opeq2d	$⊢ b = d \to ⟨suc c, c F b⟩ = ⟨suc c, c F d⟩$
6	3 5	cbvmpov	$⊢ (a \in ω, b \in V ⟼ ⟨suc a, a F b⟩) = (c \in ω, d \in V ⟼ ⟨suc c, c F d⟩)$
7		rdgeq1	$⊢ (a \in ω, b \in V ⟼ ⟨suc a, a F b⟩) = (c \in ω, d \in V ⟼ ⟨suc c, c F d⟩) \to rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) = rec ((c \in ω, d \in V ⟼ ⟨suc c, c F d⟩), ⟨\emptyset, I (I)⟩)$
8	6 7	ax-mp	$⊢ rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) = rec ((c \in ω, d \in V ⟼ ⟨suc c, c F d⟩), ⟨\emptyset, I (I)⟩)$

Metamath Proof Explorer