Metamath Proof Explorer

Theorem sbiedALT

Description: Alternate version of sbied . (Contributed by NM, 30-Jun-1994) (Revised by Mario Carneiro, 4-Oct-2016) (Proof shortened by Wolf Lammen, 24-Jun-2018) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	dfsb1.s5	$⊢ τ \leftrightarrow ((x = y \to ψ) \land \exists x (x = y \land ψ))$
		sbiedALT.1	$⊢ Ⅎ x φ$
		sbiedALT.2	$⊢ φ \to Ⅎ x χ$
		sbiedALT.3	$⊢ φ \to (x = y \to (ψ \leftrightarrow χ))$
	Assertion	sbiedALT	$⊢ φ \to (τ \leftrightarrow χ)$

Proof

Step	Hyp	Ref	Expression
1		dfsb1.s5	$⊢ τ \leftrightarrow ((x = y \to ψ) \land \exists x (x = y \land ψ))$
2		sbiedALT.1	$⊢ Ⅎ x φ$
3		sbiedALT.2	$⊢ φ \to Ⅎ x χ$
4		sbiedALT.3	$⊢ φ \to (x = y \to (ψ \leftrightarrow χ))$
5		biid	$⊢ ((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ))) \leftrightarrow ((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ)))$
6	1 5 2	sbrimALT	$⊢ ((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ))) \leftrightarrow (φ \to τ)$
7	2 3	nfim1	$⊢ Ⅎ x (φ \to χ)$
8	4	com12	$⊢ x = y \to (φ \to (ψ \leftrightarrow χ))$
9	8	pm5.74d	$⊢ x = y \to ((φ \to ψ) \leftrightarrow (φ \to χ))$
10	5 7 9	sbieALT	$⊢ ((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ))) \leftrightarrow (φ \to χ)$
11	6 10	bitr3i	$⊢ (φ \to τ) \leftrightarrow (φ \to χ)$
12	11	pm5.74ri	$⊢ φ \to (τ \leftrightarrow χ)$