subsym1

		Ref	Expression
	Assertion	subsym1	$⊢ [y/ x] [y/ x] ⊥ \to [y/ x] φ$

Step	Hyp	Ref	Expression
1		fal	$⊢ \neg ⊥$
2	1	intnan	$⊢ \neg (x = y \land ⊥)$
3	2	nex	$⊢ \neg \exists x (x = y \land ⊥)$
4	3	intnan	$⊢ \neg ((x = y \to ⊥) \land \exists x (x = y \land ⊥))$
5		dfsb1	$⊢ [y/ x] ⊥ \leftrightarrow ((x = y \to ⊥) \land \exists x (x = y \land ⊥))$
6	4 5	mtbir	$⊢ \neg [y/ x] ⊥$
7	6	intnan	$⊢ \neg (x = y \land [y/ x] ⊥)$
8	7	nex	$⊢ \neg \exists x (x = y \land [y/ x] ⊥)$
9	8	intnan	$⊢ \neg ((x = y \to [y/ x] ⊥) \land \exists x (x = y \land [y/ x] ⊥))$
10		dfsb1	$⊢ [y/ x] [y/ x] ⊥ \leftrightarrow ((x = y \to [y/ x] ⊥) \land \exists x (x = y \land [y/ x] ⊥))$
11	9 10	mtbir	$⊢ \neg [y/ x] [y/ x] ⊥$
12	11	pm2.21i	$⊢ [y/ x] [y/ x] ⊥ \to [y/ x] φ$

Metamath Proof Explorer