sbbivOLD

Description: Obsolete version of sbbi as of 24-Jul-2023. Substitution distributes over a biconditional. Version of sbbi with a disjoint variable condition, not requiring ax-11 nor ax-13 . (Contributed by Wolf Lammen, 18-Jan-2023) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dfbi2	$⊢ (φ \leftrightarrow ψ) \leftrightarrow ((φ \to ψ) \land (ψ \to φ))$
2	1	sbbii	$⊢ [y/ x] (φ \leftrightarrow ψ) \leftrightarrow [y/ x] ((φ \to ψ) \land (ψ \to φ))$
3		sbimvOLD	$⊢ [y/ x] (φ \to ψ) \leftrightarrow ([y/ x] φ \to [y/ x] ψ)$
4		sbimvOLD	$⊢ [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		sbanvOLD	$⊢ [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

Theorem sbbivOLD

Proof