Metamath Proof Explorer

Theorem sbieALT

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

		Ref	Expression
	Hypotheses	dfsb1.p7	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
		sbieALT.1	$⊢ Ⅎ x ψ$
		sbieALT.2	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	sbieALT	$⊢ θ \leftrightarrow ψ$

Proof

Step	Hyp	Ref	Expression
1		dfsb1.p7	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
2		sbieALT.1	$⊢ Ⅎ x ψ$
3		sbieALT.2	$⊢ x = y \to (φ \leftrightarrow ψ)$
4		biid	$⊢ ((x = y \to x = y) \land \exists x (x = y \land x = y)) \leftrightarrow ((x = y \to x = y) \land \exists x (x = y \land x = y))$
5	4	equsb1ALT	$⊢ ((x = y \to x = y) \land \exists x (x = y \land x = y))$
6		biid	$⊢ ((x = y \to (φ \leftrightarrow ψ)) \land \exists x (x = y \land (φ \leftrightarrow ψ))) \leftrightarrow ((x = y \to (φ \leftrightarrow ψ)) \land \exists x (x = y \land (φ \leftrightarrow ψ)))$
7	4 6 3	sbimiALT	$⊢ ((x = y \to x = y) \land \exists x (x = y \land x = y)) \to ((x = y \to (φ \leftrightarrow ψ)) \land \exists x (x = y \land (φ \leftrightarrow ψ)))$
8	5 7	ax-mp	$⊢ ((x = y \to (φ \leftrightarrow ψ)) \land \exists x (x = y \land (φ \leftrightarrow ψ)))$
9		biid	$⊢ ((x = y \to ψ) \land \exists x (x = y \land ψ)) \leftrightarrow ((x = y \to ψ) \land \exists x (x = y \land ψ))$
10	9 2	sbfALT	$⊢ ((x = y \to ψ) \land \exists x (x = y \land ψ)) \leftrightarrow ψ$
11	1 9 6 10	sblbisALT	$⊢ ((x = y \to (φ \leftrightarrow ψ)) \land \exists x (x = y \land (φ \leftrightarrow ψ))) \leftrightarrow (θ \leftrightarrow ψ)$
12	8 11	mpbi	$⊢ θ \leftrightarrow ψ$