cbvriota

Description: Change bound variable in a restricted description binder. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvriotaw when possible. (Contributed by NM, 18-Mar-2013) (Revised by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbvriota.1	$⊢ Ⅎ y φ$
	cbvriota.2	$⊢ Ⅎ x ψ$
	cbvriota.3	$⊢ x = y \to (φ \leftrightarrow ψ)$
Assertion	cbvriota	$⊢ (ι x \in A \| φ) = (ι y \in A \| ψ)$

Proof

Step	Hyp	Ref	Expression
1		cbvriota.1	$⊢ Ⅎ y φ$
2		cbvriota.2	$⊢ Ⅎ x ψ$
3		cbvriota.3	$⊢ x = y \to (φ \leftrightarrow ψ)$
4		eleq1w	$⊢ x = z \to (x \in A \leftrightarrow z \in A)$
5		sbequ12	$⊢ x = z \to (φ \leftrightarrow [z/ x] φ)$
6	4 5	anbi12d	$⊢ x = z \to ((x \in A \land φ) \leftrightarrow (z \in A \land [z/ x] φ))$
7		nfv	$⊢ Ⅎ z (x \in A \land φ)$
8		nfv	$⊢ Ⅎ x z \in A$
9		nfs1v	$⊢ Ⅎ x [z/ x] φ$
10	8 9	nfan	$⊢ Ⅎ x (z \in A \land [z/ x] φ)$
11	6 7 10	cbviota	$⊢ (ι x \| (x \in A \land φ)) = (ι z \| (z \in A \land [z/ x] φ))$
12		eleq1w	$⊢ z = y \to (z \in A \leftrightarrow y \in A)$
13		sbequ	$⊢ z = y \to ([z/ x] φ \leftrightarrow [y/ x] φ)$
14	2 3	sbie	$⊢ [y/ x] φ \leftrightarrow ψ$
15	13 14	bitrdi	$⊢ z = y \to ([z/ x] φ \leftrightarrow ψ)$
16	12 15	anbi12d	$⊢ z = y \to ((z \in A \land [z/ x] φ) \leftrightarrow (y \in A \land ψ))$
17		nfv	$⊢ Ⅎ y z \in A$
18	1	nfsb	$⊢ Ⅎ y [z/ x] φ$
19	17 18	nfan	$⊢ Ⅎ y (z \in A \land [z/ x] φ)$
20		nfv	$⊢ Ⅎ z (y \in A \land ψ)$
21	16 19 20	cbviota	$⊢ (ι z \| (z \in A \land [z/ x] φ)) = (ι y \| (y \in A \land ψ))$
22	11 21	eqtri	$⊢ (ι x \| (x \in A \land φ)) = (ι y \| (y \in A \land ψ))$
23		df-riota	$⊢ (ι x \in A \| φ) = (ι x \| (x \in A \land φ))$
24		df-riota	$⊢ (ι y \in A \| ψ) = (ι y \| (y \in A \land ψ))$
25	22 23 24	3eqtr4i	$⊢ (ι x \in A \| φ) = (ι y \in A \| ψ)$

Metamath Proof Explorer

Theorem cbvriota

Proof