cbv2

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . See cbv2w with disjoint variable conditions, not depending on ax-13 . (Contributed by NM, 5-Aug-1993) (Revised by Mario Carneiro, 3-Oct-2016) Format hypotheses to common style, avoid ax-10 . (Revised by Wolf Lammen, 10-Sep-2023) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbv2.1	$⊢ Ⅎ x φ$
	cbv2.2	$⊢ Ⅎ y φ$
	cbv2.3	$⊢ φ \to Ⅎ y ψ$
	cbv2.4	$⊢ φ \to Ⅎ x χ$
	cbv2.5	$⊢ φ \to (x = y \to (ψ \leftrightarrow χ))$
Assertion	cbv2	$⊢ φ \to (\forall x ψ \leftrightarrow \forall y χ)$

Proof

Step	Hyp	Ref	Expression
1		cbv2.1	$⊢ Ⅎ x φ$
2		cbv2.2	$⊢ Ⅎ y φ$
3		cbv2.3	$⊢ φ \to Ⅎ y ψ$
4		cbv2.4	$⊢ φ \to Ⅎ x χ$
5		cbv2.5	$⊢ φ \to (x = y \to (ψ \leftrightarrow χ))$
6		biimp	$⊢ (ψ \leftrightarrow χ) \to (ψ \to χ)$
7	5 6	syl6	$⊢ φ \to (x = y \to (ψ \to χ))$
8	1 2 3 4 7	cbv1	$⊢ φ \to (\forall x ψ \to \forall y χ)$
9		equcomi	$⊢ y = x \to x = y$
10		biimpr	$⊢ (ψ \leftrightarrow χ) \to (χ \to ψ)$
11	9 5 10	syl56	$⊢ φ \to (y = x \to (χ \to ψ))$
12	2 1 4 3 11	cbv1	$⊢ φ \to (\forall y χ \to \forall x ψ)$
13	8 12	impbid	$⊢ φ \to (\forall x ψ \leftrightarrow \forall y χ)$

Metamath Proof Explorer

Theorem cbv2

Proof