dfsb2

Description: An alternate definition of proper substitution that, like dfsb1 , mixes free and bound variables to avoid distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 17-Feb-2005) (New usage is discouraged.)

		Ref	Expression
	Assertion	dfsb2	$⊢ [y/ x] φ \leftrightarrow ((x = y \land φ) \lor \forall x (x = y \to φ))$

Proof

Step	Hyp	Ref	Expression
1		sp	$⊢ \forall x x = y \to x = y$
2		sbequ2	$⊢ x = y \to ([y/ x] φ \to φ)$
3	2	sps	$⊢ \forall x x = y \to ([y/ x] φ \to φ)$
4		orc	$⊢ (x = y \land φ) \to ((x = y \land φ) \lor \forall x (x = y \to φ))$
5	1 3 4	syl6an	$⊢ \forall x x = y \to ([y/ x] φ \to ((x = y \land φ) \lor \forall x (x = y \to φ)))$
6		sb4b	$⊢ \neg \forall x x = y \to ([y/ x] φ \leftrightarrow \forall x (x = y \to φ))$
7		olc	$⊢ \forall x (x = y \to φ) \to ((x = y \land φ) \lor \forall x (x = y \to φ))$
8	6 7	syl6bi	$⊢ \neg \forall x x = y \to ([y/ x] φ \to ((x = y \land φ) \lor \forall x (x = y \to φ)))$
9	5 8	pm2.61i	$⊢ [y/ x] φ \to ((x = y \land φ) \lor \forall x (x = y \to φ))$
10		sbequ1	$⊢ x = y \to (φ \to [y/ x] φ)$
11	10	imp	$⊢ (x = y \land φ) \to [y/ x] φ$
12		sb2	$⊢ \forall x (x = y \to φ) \to [y/ x] φ$
13	11 12	jaoi	$⊢ ((x = y \land φ) \lor \forall x (x = y \to φ)) \to [y/ x] φ$
14	9 13	impbii	$⊢ [y/ x] φ \leftrightarrow ((x = y \land φ) \lor \forall x (x = y \to φ))$

Metamath Proof Explorer

Theorem dfsb2

Proof