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) (Revised by Gino Giotto, 10-Jan-2024)

	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		nfv	$⊢ Ⅎ z (x \in A \land φ)$
7	1	nfcri	$⊢ Ⅎ x z \in A$
8		nfs1v	$⊢ Ⅎ x [z/ x] φ$
9	7 8	nfan	$⊢ Ⅎ x (z \in A \land [z/ x] φ)$
10		eleq1w	$⊢ x = z \to (x \in A \leftrightarrow z \in A)$
11		sbequ12	$⊢ x = z \to (φ \leftrightarrow [z/ x] φ)$
12	10 11	anbi12d	$⊢ x = z \to ((x \in A \land φ) \leftrightarrow (z \in A \land [z/ x] φ))$
13	6 9 12	cbvabw	$⊢ \{x \| (x \in A \land φ)\} = \{z \| (z \in A \land [z/ x] φ)\}$
14	2	nfcri	$⊢ Ⅎ y z \in A$
15	3	nfsbv	$⊢ Ⅎ y [z/ x] φ$
16	14 15	nfan	$⊢ Ⅎ y (z \in A \land [z/ x] φ)$
17		nfv	$⊢ Ⅎ z (y \in A \land ψ)$
18		eleq1w	$⊢ z = y \to (z \in A \leftrightarrow y \in A)$
19		sbequ	$⊢ z = y \to ([z/ x] φ \leftrightarrow [y/ x] φ)$
20	4 5	sbiev	$⊢ [y/ x] φ \leftrightarrow ψ$
21	19 20	bitrdi	$⊢ z = y \to ([z/ x] φ \leftrightarrow ψ)$
22	18 21	anbi12d	$⊢ z = y \to ((z \in A \land [z/ x] φ) \leftrightarrow (y \in A \land ψ))$
23	16 17 22	cbvabw	$⊢ \{z \| (z \in A \land [z/ x] φ)\} = \{y \| (y \in A \land ψ)\}$
24	13 23	eqtri	$⊢ \{x \| (x \in A \land φ)\} = \{y \| (y \in A \land ψ)\}$
25		df-rab	$⊢ \{x \in A \| φ\} = \{x \| (x \in A \land φ)\}$
26		df-rab	$⊢ \{y \in A \| ψ\} = \{y \| (y \in A \land ψ)\}$
27	24 25 26	3eqtr4i	$⊢ \{x \in A \| φ\} = \{y \in A \| ψ\}$

Metamath Proof Explorer

Theorem cbvrabw

Proof