Metamath Proof Explorer

Theorem sb6fALT

Description: Alternate version of sb6f . (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 4-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	dfsb1.p5	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
		sb6fALT.1	$⊢ Ⅎ y φ$
	Assertion	sb6fALT	$⊢ θ \leftrightarrow \forall x (x = y \to φ)$

Proof

Step	Hyp	Ref	Expression
1		dfsb1.p5	$⊢ θ \leftrightarrow ((x = y \to φ) \land \exists x (x = y \land φ))$
2		sb6fALT.1	$⊢ Ⅎ y φ$
3		biid	$⊢ ((x = y \to \forall y φ) \land \exists x (x = y \land \forall y φ)) \leftrightarrow ((x = y \to \forall y φ) \land \exists x (x = y \land \forall y φ))$
4	2	nf5ri	$⊢ φ \to \forall y φ$
5	1 3 4	sbimiALT	$⊢ θ \to ((x = y \to \forall y φ) \land \exists x (x = y \land \forall y φ))$
6	3	sb4aALT	$⊢ ((x = y \to \forall y φ) \land \exists x (x = y \land \forall y φ)) \to \forall x (x = y \to φ)$
7	5 6	syl	$⊢ θ \to \forall x (x = y \to φ)$
8	1	sb2ALT	$⊢ \forall x (x = y \to φ) \to θ$
9	7 8	impbii	$⊢ θ \leftrightarrow \forall x (x = y \to φ)$