Metamath Proof Explorer

Theorem sb5ALT

Description: Equivalence for substitution. Alternate proof of sb5 . This proof is sb5ALTVD automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	sb5ALT	$⊢ [y/ x] φ \leftrightarrow \exists x (x = y \land φ)$

Proof

Step	Hyp	Ref	Expression
1		equsb1	$⊢ [y/ x] x = y$
2		sban	$⊢ [y/ x] (x = y \land φ) \leftrightarrow ([y/ x] x = y \land [y/ x] φ)$
3	2	simplbi2com	$⊢ [y/ x] φ \to ([y/ x] x = y \to [y/ x] (x = y \land φ))$
4	1 3	mpi	$⊢ [y/ x] φ \to [y/ x] (x = y \land φ)$
5		spsbe	$⊢ [y/ x] (x = y \land φ) \to \exists x (x = y \land φ)$
6	4 5	syl	$⊢ [y/ x] φ \to \exists x (x = y \land φ)$
7		hbs1	$⊢ [y/ x] φ \to \forall x [y/ x] φ$
8		simpr	$⊢ (x = y \land φ) \to φ$
9	8	a1i	$⊢ \exists x (x = y \land φ) \to ((x = y \land φ) \to φ)$
10		simpl	$⊢ (x = y \land φ) \to x = y$
11	10	a1i	$⊢ \exists x (x = y \land φ) \to ((x = y \land φ) \to x = y)$
12		sbequ1	$⊢ x = y \to (φ \to [y/ x] φ)$
13	12	com12	$⊢ φ \to (x = y \to [y/ x] φ)$
14	9 11 13	syl6c	$⊢ \exists x (x = y \land φ) \to ((x = y \land φ) \to [y/ x] φ)$
15	7 14	exlimexi	$⊢ \exists x (x = y \land φ) \to [y/ x] φ$
16	6 15	impbii	$⊢ [y/ x] φ \leftrightarrow \exists x (x = y \land φ)$