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	sbbiiev	$⊢ [y/ x] (x \in A \to φ) \leftrightarrow [y/ x] (y \in A \to φ)$
7		sbrimvw	$⊢ [y/ x] (y \in A \to φ) \leftrightarrow (y \in A \to [y/ x] φ)$
8	6 7	bitr2i	$⊢ (y \in A \to [y/ x] φ) \leftrightarrow [y/ x] (x \in A \to φ)$
9	8	albii	$⊢ \forall y (y \in A \to [y/ x] φ) \leftrightarrow \forall y [y/ x] (x \in A \to φ)$
10	3 9	bitri	$⊢ \forall y \in A [y/ x] φ \leftrightarrow \forall y [y/ x] (x \in A \to φ)$
11	1 2 10	3bitr4i	$⊢ \forall x \in A φ \leftrightarrow \forall y \in A [y/ x] φ$

Metamath Proof Explorer

Theorem cbvralsvw

Proof