Metamath Proof Explorer

Theorem dfsb7OLD

Description: Obsolete version of dfsb7 as of 3-Sep-2023. (Contributed by NM, 28-Jan-2004) Revise df-sb . (Revised by BJ, 25-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-sb	$⊢ [t/ x] φ \leftrightarrow \forall y (y = t \to \forall x (x = y \to φ))$
2		sb56	$⊢ \exists y (y = t \land \forall x (x = y \to φ)) \leftrightarrow \forall y (y = t \to \forall x (x = y \to φ))$
3		sb56	$⊢ \exists x (x = y \land φ) \leftrightarrow \forall x (x = y \to φ)$
4	3	bicomi	$⊢ \forall x (x = y \to φ) \leftrightarrow \exists x (x = y \land φ)$
5	4	anbi2i	$⊢ (y = t \land \forall x (x = y \to φ)) \leftrightarrow (y = t \land \exists x (x = y \land φ))$
6	5	exbii	$⊢ \exists y (y = t \land \forall x (x = y \to φ)) \leftrightarrow \exists y (y = t \land \exists x (x = y \land φ))$
7	1 2 6	3bitr2i	$⊢ [t/ x] φ \leftrightarrow \exists y (y = t \land \exists x (x = y \land φ))$