bj-ax12ssb

Description: Axiom bj-ax12 expressed using substitution. (Contributed by BJ, 26-Dec-2020) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	bj-ax12ssb	$⊢ [t/ x] (φ \to [t/ x] φ)$

Step	Hyp	Ref	Expression
1		bj-ax12	$⊢ \forall x (x = t \to (φ \to \forall x (x = t \to φ)))$
2		sb6	$⊢ [t/ x] φ \leftrightarrow \forall x (x = t \to φ)$
3	2	imbi2i	$⊢ (φ \to [t/ x] φ) \leftrightarrow (φ \to \forall x (x = t \to φ))$
4	3	imbi2i	$⊢ (x = t \to (φ \to [t/ x] φ)) \leftrightarrow (x = t \to (φ \to \forall x (x = t \to φ)))$
5	4	albii	$⊢ \forall x (x = t \to (φ \to [t/ x] φ)) \leftrightarrow \forall x (x = t \to (φ \to \forall x (x = t \to φ)))$
6	1 5	mpbir	$⊢ \forall x (x = t \to (φ \to [t/ x] φ))$
7		sb6	$⊢ [t/ x] (φ \to [t/ x] φ) \leftrightarrow \forall x (x = t \to (φ \to [t/ x] φ))$
8	6 7	mpbir	$⊢ [t/ x] (φ \to [t/ x] φ)$

Metamath Proof Explorer