bj-substax12

Description: Equivalent form of the axiom of substitution bj-ax12 . Although both sides need a DV condition on x , t (or as in bj-ax12v3 on t , ph ) to hold, their equivalence holds without DV conditions. The forward implication is proved in modal (K4) while the reverse implication is proved in modal (T5). The LHS has the advantage of not involving nested quantifiers on the same variable. Its metaweakening is proved from the core axiom schemes in bj-substw . Note that in the LHS, the reverse implication holds by equs4 (or equs4v if a DV condition is added on x , t as in bj-ax12 ), and the forward implication is sbalex .

The LHS can be read as saying that if there exists a variable equal to a given term witnessing a given formula, then all variables equal to that term also witness that formula. The equivalent form of the LHS using only primitive symbols is ( A. x ( x = t -> ph ) \/ A. x ( x = t -> -. ph ) ) , which expresses that a given formula is true at all variables equal to a given term, or false at all these variables. An equivalent form of the LHS using only the existential quantifier is -. ( E. x ( x = t /\ ph ) /\ E. x ( x = t /\ -. ph ) ) , which expresses that there can be no two variables both equal to a given term, one witnessing a formula and the other witnessing its negation. These equivalences do not hold in intuitionistic logic. The LHS should be the preferred form, and has the advantage of having no negation nor nested quantifiers. (Contributed by BJ, 21-May-2024) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	bj-substax12	$⊢ (\exists x (x = t \land φ) \to \forall x (x = t \to φ)) \leftrightarrow \forall x (x = t \to (φ \to \forall x (x = t \to φ)))$

Proof

Step	Hyp	Ref	Expression
1		bj-modal4	$⊢ \forall x (x = t \to φ) \to \forall x \forall x (x = t \to φ)$
2	1	imim2i	$⊢ (\exists x (x = t \land φ) \to \forall x (x = t \to φ)) \to (\exists x (x = t \land φ) \to \forall x \forall x (x = t \to φ))$
3		19.38	$⊢ (\exists x (x = t \land φ) \to \forall x \forall x (x = t \to φ)) \to \forall x ((x = t \land φ) \to \forall x (x = t \to φ))$
4	2 3	syl	$⊢ (\exists x (x = t \land φ) \to \forall x (x = t \to φ)) \to \forall x ((x = t \land φ) \to \forall x (x = t \to φ))$
5		hbe1a	$⊢ \exists x \forall x (x = t \to φ) \to \forall x (x = t \to φ)$
6	5 1	syl	$⊢ \exists x \forall x (x = t \to φ) \to \forall x \forall x (x = t \to φ)$
7		bj-exlimg	$⊢ (\exists x \forall x (x = t \to φ) \to \forall x \forall x (x = t \to φ)) \to (\forall x ((x = t \land φ) \to \forall x (x = t \to φ)) \to (\exists x (x = t \land φ) \to \forall x \forall x (x = t \to φ)))$
8	6 7	ax-mp	$⊢ \forall x ((x = t \land φ) \to \forall x (x = t \to φ)) \to (\exists x (x = t \land φ) \to \forall x \forall x (x = t \to φ))$
9		sp	$⊢ \forall x \forall x (x = t \to φ) \to \forall x (x = t \to φ)$
10	9	imim2i	$⊢ (\exists x (x = t \land φ) \to \forall x \forall x (x = t \to φ)) \to (\exists x (x = t \land φ) \to \forall x (x = t \to φ))$
11	8 10	syl	$⊢ \forall x ((x = t \land φ) \to \forall x (x = t \to φ)) \to (\exists x (x = t \land φ) \to \forall x (x = t \to φ))$
12	4 11	impbii	$⊢ (\exists x (x = t \land φ) \to \forall x (x = t \to φ)) \leftrightarrow \forall x ((x = t \land φ) \to \forall x (x = t \to φ))$
13		impexp	$⊢ ((x = t \land φ) \to \forall x (x = t \to φ)) \leftrightarrow (x = t \to (φ \to \forall x (x = t \to φ)))$
14	13	albii	$⊢ \forall x ((x = t \land φ) \to \forall x (x = t \to φ)) \leftrightarrow \forall x (x = t \to (φ \to \forall x (x = t \to φ)))$
15	12 14	bitri	$⊢ (\exists x (x = t \land φ) \to \forall x (x = t \to φ)) \leftrightarrow \forall x (x = t \to (φ \to \forall x (x = t \to φ)))$

Metamath Proof Explorer

Theorem bj-substax12

Proof