dfsb2ALT

Description: Alternate version of dfsb2 . (Contributed by NM, 17-Feb-2005) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	dfsb1.ph	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
	Assertion	dfsb2ALT	$⊢ θ \leftrightarrow ((x = y \land φ) \lor \forall x (x = y \to φ))$

Step	Hyp	Ref	Expression
1		dfsb1.ph	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
2		sp	$⊢ \forall x x = y \to x = y$
3	1	sbequ2ALT	$⊢ x = y \to (θ \to φ)$
4	3	sps	$⊢ \forall x x = y \to (θ \to φ)$
5		orc	$⊢ (x = y \land φ) \to ((x = y \land φ) \lor \forall x (x = y \to φ))$
6	2 4 5	syl6an	$⊢ \forall x x = y \to (θ \to ((x = y \land φ) \lor \forall x (x = y \to φ)))$
7	1	sb4ALT	$⊢ \neg \forall x x = y \to (θ \to \forall x (x = y \to φ))$
8		olc	$⊢ \forall x (x = y \to φ) \to ((x = y \land φ) \lor \forall x (x = y \to φ))$
9	7 8	syl6	$⊢ \neg \forall x x = y \to (θ \to ((x = y \land φ) \lor \forall x (x = y \to φ)))$
10	6 9	pm2.61i	$⊢ θ \to ((x = y \land φ) \lor \forall x (x = y \to φ))$
11	1	sbequ1ALT	$⊢ x = y \to (φ \to θ)$
12	11	imp	$⊢ (x = y \land φ) \to θ$
13	1	sb2ALT	$⊢ \forall x (x = y \to φ) \to θ$
14	12 13	jaoi	$⊢ ((x = y \land φ) \lor \forall x (x = y \to φ)) \to θ$
15	10 14	impbii	$⊢ θ \leftrightarrow ((x = y \land φ) \lor \forall x (x = y \to φ))$

Metamath Proof Explorer