cbvrabw

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 11-Jul-2011) Avoid ax-13 . (Revised by GG, 10-Jan-2024) Avoid ax-10 . (Revised by Wolf Lammen, 19-Jul-2025)

	Ref	Expression
Hypotheses	cbvrabw.1	$⊢ \underline{Ⅎ} x A$
	cbvrabw.2	$⊢ \underline{Ⅎ} y A$
	cbvrabw.3	$⊢ Ⅎ y φ$
	cbvrabw.4	$⊢ Ⅎ x ψ$
	cbvrabw.5	$⊢ x = y \to (φ \leftrightarrow ψ)$
Assertion	cbvrabw	$⊢ \{x \in A \| φ\} = \{y \in A \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		cbvrabw.1	$⊢ \underline{Ⅎ} x A$
2		cbvrabw.2	$⊢ \underline{Ⅎ} y A$
3		cbvrabw.3	$⊢ Ⅎ y φ$
4		cbvrabw.4	$⊢ Ⅎ x ψ$
5		cbvrabw.5	$⊢ x = y \to (φ \leftrightarrow ψ)$
6	2	nfcri	$⊢ Ⅎ y x \in A$
7	6 3	nfan	$⊢ Ⅎ y (x \in A \land φ)$
8	1	nfcri	$⊢ Ⅎ x y \in A$
9	8 4	nfan	$⊢ Ⅎ x (y \in A \land ψ)$
10		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
11	10 5	anbi12d	$⊢ x = y \to ((x \in A \land φ) \leftrightarrow (y \in A \land ψ))$
12	7 9 11	cbvabw	$⊢ \{x \| (x \in A \land φ)\} = \{y \| (y \in A \land ψ)\}$
13		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
14		df-rab	$⊢ \{y \in A \| ψ\} = \{y \| (y \in A \land ψ)\}$
15	12 13 14	3eqtr4i	$⊢ \{x \in A \| φ\} = \{y \in A \| ψ\}$

Metamath Proof Explorer

Theorem cbvrabw

Proof