Metamath Proof Explorer

Theorem sbrimALT

Description: Alternate version of sbrim . (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 4-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	dfsb1.s3	$⊢ τ \leftrightarrow ((x = y \to ψ) \land \exists x (x = y \land ψ))$
		dfsb1.i2	$⊢ η \leftrightarrow ((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ)))$
		sbrimALT.1	$⊢ Ⅎ x φ$
	Assertion	sbrimALT	$⊢ η \leftrightarrow (φ \to τ)$

Proof

Step	Hyp	Ref	Expression
1		dfsb1.s3	$⊢ τ \leftrightarrow ((x = y \to ψ) \land \exists x (x = y \land ψ))$
2		dfsb1.i2	$⊢ η \leftrightarrow ((x = y \to (φ \to ψ)) \land \exists x (x = y \land (φ \to ψ)))$
3		sbrimALT.1	$⊢ Ⅎ x φ$
4		biid	$⊢ ((x = y \to φ) \land \exists x (x = y \land φ)) \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
5	4 1 2	sbimALT	$⊢ η \leftrightarrow (((x = y \to φ) \land \exists x (x = y \land φ)) \to τ)$
6	4 3	sbfALT	$⊢ ((x = y \to φ) \land \exists x (x = y \land φ)) \leftrightarrow φ$
7	6	imbi1i	$⊢ (((x = y \to φ) \land \exists x (x = y \land φ)) \to τ) \leftrightarrow (φ \to τ)$
8	5 7	bitri	$⊢ η \leftrightarrow (φ \to τ)$