sbrimvlem

Description: Common proof template for sbrimvw and sbrimv . The hypothesis is an instance of 19.21 . (Contributed by Wolf Lammen, 29-Jan-2024)

		Ref	Expression
	Hypothesis	sbrimvlem.1	$⊢ \forall x (φ \to (x = y \to ψ)) \leftrightarrow (φ \to \forall x (x = y \to ψ))$
	Assertion	sbrimvlem	$⊢ [y/ x] (φ \to ψ) \leftrightarrow (φ \to [y/ x] ψ)$

Step	Hyp	Ref	Expression
1		sbrimvlem.1	$⊢ \forall x (φ \to (x = y \to ψ)) \leftrightarrow (φ \to \forall x (x = y \to ψ))$
2		sb6	$⊢ [y/ x] (φ \to ψ) \leftrightarrow \forall x (x = y \to (φ \to ψ))$
3		bi2.04	$⊢ (φ \to (x = y \to ψ)) \leftrightarrow (x = y \to (φ \to ψ))$
4	3	albii	$⊢ \forall x (φ \to (x = y \to ψ)) \leftrightarrow \forall x (x = y \to (φ \to ψ))$
5	2 4 1	3bitr2i	$⊢ [y/ x] (φ \to ψ) \leftrightarrow (φ \to \forall x (x = y \to ψ))$
6		sb6	$⊢ [y/ x] ψ \leftrightarrow \forall x (x = y \to ψ)$
7	6	imbi2i	$⊢ (φ \to [y/ x] ψ) \leftrightarrow (φ \to \forall x (x = y \to ψ))$
8	5 7	bitr4i	$⊢ [y/ x] (φ \to ψ) \leftrightarrow (φ \to [y/ x] ψ)$

Metamath Proof Explorer