bj-subst

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 ).

The LHS can be read as saying that if there exists a setvar equal to a given term witnessing ph , then all setvars equal to that term also witness ph . An equivalent suggestive form for the LHS 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 ph and the other witnessing -. ph . (Contributed by BJ, 21-May-2024) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	bj-subst	$⊢ (\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-subst

Proof