cbvriotaw

Description: Change bound variable in a restricted description binder. Version of cbvriota with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 18-Mar-2013) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvriotaw.1	$⊢ Ⅎ y φ$
2		cbvriotaw.2	$⊢ Ⅎ x ψ$
3		cbvriotaw.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	cbviotaw	$⊢ (ι 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	2 3	sbhypf	$⊢ z = y \to ([z/ x] φ \leftrightarrow ψ)$
14	12 13	anbi12d	$⊢ z = y \to ((z \in A \land [z/ x] φ) \leftrightarrow (y \in A \land ψ))$
15		nfv	$⊢ Ⅎ y z \in A$
16	1	nfsbv	$⊢ Ⅎ y [z/ x] φ$
17	15 16	nfan	$⊢ Ⅎ y (z \in A \land [z/ x] φ)$
18		nfv	$⊢ Ⅎ z (y \in A \land ψ)$
19	14 17 18	cbviotaw	$⊢ (ι z \| (z \in A \land [z/ x] φ)) = (ι y \| (y \in A \land ψ))$
20	11 19	eqtri	$⊢ (ι x \| (x \in A \land φ)) = (ι y \| (y \in A \land ψ))$
21		df-riota	$⊢ (ι x \in A \| φ) = (ι x \| (x \in A \land φ))$
22		df-riota	$⊢ (ι y \in A \| ψ) = (ι y \| (y \in A \land ψ))$
23	20 21 22	3eqtr4i	$⊢ (ι x \in A \| φ) = (ι y \in A \| ψ)$

Metamath Proof Explorer

Theorem cbvriotaw

Proof