sbequiALT

Description: Alternate version of sbequi . (Contributed by NM, 14-May-1993) (Proof shortened by Wolf Lammen, 15-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dfsb1.xz	$⊢ θ \leftrightarrow ((z = x \to φ) \land \exists z (z = x \land φ))$
	dfsb1.yz	$⊢ τ \leftrightarrow ((z = y \to φ) \land \exists z (z = y \land φ))$
Assertion	sbequiALT	$⊢ x = y \to (θ \to τ)$

Proof

Step	Hyp	Ref	Expression
1		dfsb1.xz	$⊢ θ \leftrightarrow ((z = x \to φ) \land \exists z (z = x \land φ))$
2		dfsb1.yz	$⊢ τ \leftrightarrow ((z = y \to φ) \land \exists z (z = y \land φ))$
3		equtr	$⊢ z = x \to (x = y \to z = y)$
4	1	sbequ2ALT	$⊢ z = x \to (θ \to φ)$
5	2	sbequ1ALT	$⊢ z = y \to (φ \to τ)$
6	4 5	syl9	$⊢ z = x \to (z = y \to (θ \to τ))$
7	3 6	syld	$⊢ z = x \to (x = y \to (θ \to τ))$
8		ax13	$⊢ \neg z = x \to (x = y \to \forall z x = y)$
9		sp	$⊢ \forall z z = x \to z = x$
10	9	con3i	$⊢ \neg z = x \to \neg \forall z z = x$
11	1	sb4ALT	$⊢ \neg \forall z z = x \to (θ \to \forall z (z = x \to φ))$
12	10 11	syl	$⊢ \neg z = x \to (θ \to \forall z (z = x \to φ))$
13		equeuclr	$⊢ x = y \to (z = y \to z = x)$
14	13	imim1d	$⊢ x = y \to ((z = x \to φ) \to (z = y \to φ))$
15	14	al2imi	$⊢ \forall z x = y \to (\forall z (z = x \to φ) \to \forall z (z = y \to φ))$
16	2	sb2ALT	$⊢ \forall z (z = y \to φ) \to τ$
17	15 16	syl6	$⊢ \forall z x = y \to (\forall z (z = x \to φ) \to τ)$
18	12 17	syl9	$⊢ \neg z = x \to (\forall z x = y \to (θ \to τ))$
19	8 18	syld	$⊢ \neg z = x \to (x = y \to (θ \to τ))$
20	7 19	pm2.61i	$⊢ x = y \to (θ \to τ)$

Metamath Proof Explorer

Theorem sbequiALT

Proof