cbvralsvw

Description: Change bound variable by using a substitution. Version of cbvralsv with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 20-Nov-2005) Avoid ax-13 . (Revised by GG, 10-Jan-2024) (Proof shortened by Wolf Lammen, 8-Mar-2025) Avoid ax-10 , ax-12 . (Revised by SN, 21-Aug-2025)

		Ref	Expression
	Assertion	cbvralsvw	$⊢ \forall x \in A φ \leftrightarrow \forall y \in A [y/ x] φ$

Proof

Step	Hyp	Ref	Expression
1		sb8v	$⊢ \forall x (x \in A \to φ) \leftrightarrow \forall y [y/ x] (x \in A \to φ)$
2		df-ral	$⊢ \forall x \in A φ \leftrightarrow \forall x (x \in A \to φ)$
3		df-ral	$⊢ \forall y \in A [y/ x] φ \leftrightarrow \forall y (y \in A \to [y/ x] φ)$
4		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
5	4	imbi1d	$⊢ x = y \to ((x \in A \to φ) \leftrightarrow (y \in A \to φ))$
6	5	pm5.74i	$⊢ (x = y \to (x \in A \to φ)) \leftrightarrow (x = y \to (y \in A \to φ))$
7	6	albii	$⊢ \forall x (x = y \to (x \in A \to φ)) \leftrightarrow \forall x (x = y \to (y \in A \to φ))$
8		sb6	$⊢ [y/ x] (x \in A \to φ) \leftrightarrow \forall x (x = y \to (x \in A \to φ))$
9		sb6	$⊢ [y/ x] (y \in A \to φ) \leftrightarrow \forall x (x = y \to (y \in A \to φ))$
10	7 8 9	3bitr4i	$⊢ [y/ x] (x \in A \to φ) \leftrightarrow [y/ x] (y \in A \to φ)$
11		sbrimvw	$⊢ [y/ x] (y \in A \to φ) \leftrightarrow (y \in A \to [y/ x] φ)$
12	10 11	bitr2i	$⊢ (y \in A \to [y/ x] φ) \leftrightarrow [y/ x] (x \in A \to φ)$
13	12	albii	$⊢ \forall y (y \in A \to [y/ x] φ) \leftrightarrow \forall y [y/ x] (x \in A \to φ)$
14	3 13	bitri	$⊢ \forall y \in A [y/ x] φ \leftrightarrow \forall y [y/ x] (x \in A \to φ)$
15	1 2 14	3bitr4i	$⊢ \forall x \in A φ \leftrightarrow \forall y \in A [y/ x] φ$

Metamath Proof Explorer

Theorem cbvralsvw

Proof