Metamath Proof Explorer

Theorem sbnALT

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

		Ref	Expression
	Hypotheses	dfsb1.ph	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
		dfsb1.n	$⊢ τ \leftrightarrow ((x = y \to \neg φ) \land \exists x (x = y \land \neg φ))$
	Assertion	sbnALT	$⊢ τ \leftrightarrow \neg θ$

Proof

Step	Hyp	Ref	Expression
1		dfsb1.ph	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
2		dfsb1.n	$⊢ τ \leftrightarrow ((x = y \to \neg φ) \land \exists x (x = y \land \neg φ))$
3		exanali	$⊢ \exists x (x = y \land \neg φ) \leftrightarrow \neg \forall x (x = y \to φ)$
4	3	anbi2i	$⊢ ((x = y \to \neg φ) \land \exists x (x = y \land \neg φ)) \leftrightarrow ((x = y \to \neg φ) \land \neg \forall x (x = y \to φ))$
5		annim	$⊢ ((x = y \to \neg φ) \land \neg \forall x (x = y \to φ)) \leftrightarrow \neg ((x = y \to \neg φ) \to \forall x (x = y \to φ))$
6	2 4 5	3bitri	$⊢ τ \leftrightarrow \neg ((x = y \to \neg φ) \to \forall x (x = y \to φ))$
7	1	dfsb3ALT	$⊢ θ \leftrightarrow ((x = y \to \neg φ) \to \forall x (x = y \to φ))$
8	6 7	xchbinxr	$⊢ τ \leftrightarrow \neg θ$