dfsb3

Description: An alternate definition of proper substitution df-sb that uses only primitive connectives (no defined terms) on the right-hand side. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 6-Mar-2007) (New usage is discouraged.)

		Ref	Expression
	Assertion	dfsb3	$⊢ [y/ x] φ \leftrightarrow ((x = y \to \neg φ) \to \forall x (x = y \to φ))$

Proof

Step	Hyp	Ref	Expression
1		df-or	$⊢ ((x = y \land φ) \lor \forall x (x = y \to φ)) \leftrightarrow (\neg (x = y \land φ) \to \forall x (x = y \to φ))$
2		dfsb2	$⊢ [y/ x] φ \leftrightarrow ((x = y \land φ) \lor \forall x (x = y \to φ))$
3		imnan	$⊢ (x = y \to \neg φ) \leftrightarrow \neg (x = y \land φ)$
4	3	imbi1i	$⊢ ((x = y \to \neg φ) \to \forall x (x = y \to φ)) \leftrightarrow (\neg (x = y \land φ) \to \forall x (x = y \to φ))$
5	1 2 4	3bitr4i	$⊢ [y/ x] φ \leftrightarrow ((x = y \to \neg φ) \to \forall x (x = y \to φ))$

Metamath Proof Explorer

Theorem dfsb3

Proof