sbbi

Description: Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993)

		Ref	Expression
	Assertion	sbbi	$⊢ [y/ x] (φ \leftrightarrow ψ) \leftrightarrow ([y/ x] φ \leftrightarrow [y/ x] ψ)$

Step	Hyp	Ref	Expression
1		dfbi2	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \to ψ) \land (ψ \to φ))$
2	1	sbbii	$⊢ [y/ x] (φ \leftrightarrow ψ) \leftrightarrow [y/ x] ((φ \to ψ) \land (ψ \to φ))$
3		sbim	$⊢ [y/ x] (φ \to ψ) \leftrightarrow ([y/ x] φ \to [y/ x] ψ)$
4		sbim	$⊢ [y/ x] (ψ \to φ) \leftrightarrow ([y/ x] ψ \to [y/ x] φ)$
5	3 4	anbi12i	$⊢ ([y/ x] (φ \to ψ) \land [y/ x] (ψ \to φ)) \leftrightarrow (([y/ x] φ \to [y/ x] ψ) \land ([y/ x] ψ \to [y/ x] φ))$
6		sban	$⊢ [y/ x] ((φ \to ψ) \land (ψ \to φ)) \leftrightarrow ([y/ x] (φ \to ψ) \land [y/ x] (ψ \to φ))$
7		dfbi2	$⊢ ([y/ x] φ \leftrightarrow [y/ x] ψ) \leftrightarrow (([y/ x] φ \to [y/ x] ψ) \land ([y/ x] ψ \to [y/ x] φ))$
8	5 6 7	3bitr4i	$⊢ [y/ x] ((φ \to ψ) \land (ψ \to φ)) \leftrightarrow ([y/ x] φ \leftrightarrow [y/ x] ψ)$
9	2 8	bitri	$⊢ [y/ x] (φ \leftrightarrow ψ) \leftrightarrow ([y/ x] φ \leftrightarrow [y/ x] ψ)$

Metamath Proof Explorer