This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rdgsucmpt2

Description: This version of rdgsucmpt avoids the not-free hypothesis of rdgsucmptf by using two substitutions instead of one. (Contributed by Mario Carneiro, 11-Sep-2015)

		Ref	Expression
	Hypotheses	rdgsucmpt2.1	$⊢ F = rec ((x \in V ⟼ C), A)$
		rdgsucmpt2.2	$⊢ y = x \to E = C$
		rdgsucmpt2.3	$⊢ y = F (B) \to E = D$
	Assertion	rdgsucmpt2	$⊢ (B \in On \land D \in V) \to F (suc B) = D$

Proof

Step	Hyp	Ref	Expression
1		rdgsucmpt2.1	$⊢ F = rec ((x \in V ⟼ C), A)$
2		rdgsucmpt2.2	$⊢ y = x \to E = C$
3		rdgsucmpt2.3	$⊢ y = F (B) \to E = D$
4		nfcv	$⊢ \underline{Ⅎ} y A$
5		nfcv	$⊢ \underline{Ⅎ} y B$
6		nfcv	$⊢ \underline{Ⅎ} y D$
7	2	cbvmptv	$⊢ (y \in V ⟼ E) = (x \in V ⟼ C)$
8		rdgeq1	$⊢ (y \in V ⟼ E) = (x \in V ⟼ C) \to rec ((y \in V ⟼ E), A) = rec ((x \in V ⟼ C), A)$
9	7 8	ax-mp	$⊢ rec ((y \in V ⟼ E), A) = rec ((x \in V ⟼ C), A)$
10	1 9	eqtr4i	$⊢ F = rec ((y \in V ⟼ E), A)$
11	4 5 6 10 3	rdgsucmptf	$⊢ (B \in On \land D \in V) \to F (suc B) = D$