sbcom3

Description: Substituting y for x and then z for y is equivalent to substituting z for both x and y . Usage of this theorem is discouraged because it depends on ax-13 . For a version requiring a disjoint variable, but fewer axioms, see sbcom3vv . (Contributed by Giovanni Mascellani, 8-Apr-2018) Remove dependency on ax-11 . (Revised by Wolf Lammen, 16-Sep-2018) (Proof shortened by Wolf Lammen, 16-Sep-2018) (New usage is discouraged.)

		Ref	Expression
	Assertion	sbcom3	$⊢ [z/ y] [y/ x] φ \leftrightarrow [z/ y] [z/ x] φ$

Proof

Step	Hyp	Ref	Expression
1		nfa1	$⊢ Ⅎ y \forall y y = z$
2		drsb2	$⊢ \forall y y = z \to ([y/ x] φ \leftrightarrow [z/ x] φ)$
3	1 2	sbbid	$⊢ \forall y y = z \to ([z/ y] [y/ x] φ \leftrightarrow [z/ y] [z/ x] φ)$
4		sb4b	$⊢ \neg \forall y y = z \to ([z/ y] [y/ x] φ \leftrightarrow \forall y (y = z \to [y/ x] φ))$
5		sbequ	$⊢ y = z \to ([y/ x] φ \leftrightarrow [z/ x] φ)$
6	5	pm5.74i	$⊢ (y = z \to [y/ x] φ) \leftrightarrow (y = z \to [z/ x] φ)$
7	6	albii	$⊢ \forall y (y = z \to [y/ x] φ) \leftrightarrow \forall y (y = z \to [z/ x] φ)$
8	4 7	bitrdi	$⊢ \neg \forall y y = z \to ([z/ y] [y/ x] φ \leftrightarrow \forall y (y = z \to [z/ x] φ))$
9		sb4b	$⊢ \neg \forall y y = z \to ([z/ y] [z/ x] φ \leftrightarrow \forall y (y = z \to [z/ x] φ))$
10	8 9	bitr4d	$⊢ \neg \forall y y = z \to ([z/ y] [y/ x] φ \leftrightarrow [z/ y] [z/ x] φ)$
11	3 10	pm2.61i	$⊢ [z/ y] [y/ x] φ \leftrightarrow [z/ y] [z/ x] φ$

Metamath Proof Explorer

Theorem sbcom3

Proof