Metamath Proof Explorer

Theorem sbco2ALT

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

		Ref	Expression
	Hypotheses	dfsb1.p8	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
		dfsb1.sb	$⊢ τ \leftrightarrow ((z = y \to ((x = z \to φ) \land \exists x (x = z \land φ))) \land \exists z (z = y \land ((x = z \to φ) \land \exists x (x = z \land φ))))$
		sbco2ALT.1	$⊢ Ⅎ z φ$
	Assertion	sbco2ALT	$⊢ τ \leftrightarrow θ$

Proof

Step	Hyp	Ref	Expression
1		dfsb1.p8	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
2		dfsb1.sb	$⊢ τ \leftrightarrow ((z = y \to ((x = z \to φ) \land \exists x (x = z \land φ))) \land \exists z (z = y \land ((x = z \to φ) \land \exists x (x = z \land φ))))$
3		sbco2ALT.1	$⊢ Ⅎ z φ$
4	2	sbequ12ALT	$⊢ z = y \to (((x = z \to φ) \land \exists x (x = z \land φ)) \leftrightarrow τ)$
5		biid	$⊢ ((x = z \to φ) \land \exists x (x = z \land φ)) \leftrightarrow ((x = z \to φ) \land \exists x (x = z \land φ))$
6	5 1	sbequALT	$⊢ z = y \to (((x = z \to φ) \land \exists x (x = z \land φ)) \leftrightarrow θ)$
7	4 6	bitr3d	$⊢ z = y \to (τ \leftrightarrow θ)$
8	7	sps	$⊢ \forall z z = y \to (τ \leftrightarrow θ)$
9		nfnae	$⊢ Ⅎ z \neg \forall z z = y$
10	1 3	nfsb4ALT	$⊢ \neg \forall z z = y \to Ⅎ z θ$
11	6	a1i	$⊢ \neg \forall z z = y \to (z = y \to (((x = z \to φ) \land \exists x (x = z \land φ)) \leftrightarrow θ))$
12	2 9 10 11	sbiedALT	$⊢ \neg \forall z z = y \to (τ \leftrightarrow θ)$
13	8 12	pm2.61i	$⊢ τ \leftrightarrow θ$