Metamath Proof Explorer

Theorem rdglem1

Description: Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use. (Contributed by NM, 9-Apr-1995)

		Ref	Expression
	Assertion	rdglem1	$⊢ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = G ({f ↾}_{y}))\} = \{g \| \exists z \in On (g Fn z \land \forall w \in z g (w) = G ({g ↾}_{w}))\}$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = G ({f ↾}_{y}))\} = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = G ({f ↾}_{y}))\}$
2	1	tfrlem3	$⊢ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = G ({f ↾}_{y}))\} = \{g \| \exists z \in On (g Fn z \land \forall v \in z g (v) = G ({g ↾}_{v}))\}$
3		fveq2	$⊢ v = w \to g (v) = g (w)$
4		reseq2	$⊢ v = w \to {g ↾}_{v} = {g ↾}_{w}$
5	4	fveq2d	$⊢ v = w \to G ({g ↾}_{v}) = G ({g ↾}_{w})$
6	3 5	eqeq12d	$⊢ v = w \to (g (v) = G ({g ↾}_{v}) \leftrightarrow g (w) = G ({g ↾}_{w}))$
7	6	cbvralvw	$⊢ \forall v \in z g (v) = G ({g ↾}_{v}) \leftrightarrow \forall w \in z g (w) = G ({g ↾}_{w})$
8	7	anbi2i	$⊢ (g Fn z \land \forall v \in z g (v) = G ({g ↾}_{v})) \leftrightarrow (g Fn z \land \forall w \in z g (w) = G ({g ↾}_{w}))$
9	8	rexbii	$⊢ \exists z \in On (g Fn z \land \forall v \in z g (v) = G ({g ↾}_{v})) \leftrightarrow \exists z \in On (g Fn z \land \forall w \in z g (w) = G ({g ↾}_{w}))$
10	9	abbii	$⊢ \{g \| \exists z \in On (g Fn z \land \forall v \in z g (v) = G ({g ↾}_{v}))\} = \{g \| \exists z \in On (g Fn z \land \forall w \in z g (w) = G ({g ↾}_{w}))\}$
11	2 10	eqtri	$⊢ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = G ({f ↾}_{y}))\} = \{g \| \exists z \in On (g Fn z \land \forall w \in z g (w) = G ({g ↾}_{w}))\}$