Theorem bj-substw

Description: Weak form of the LHS of bj-subst proved from the core axiom schemes. Compare ax12w . (Contributed by BJ, 26-May-2024) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	bj-substw.is	$$⊢x=t\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	bj-substw	$$⊢\exists x\left(x=t\wedge \phi \right)\to \forall x\left(x=t\to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-substw.is	$$⊢x=t\to \left(\phi \leftrightarrow \psi \right)$$
2	1	pm5.32i	$$⊢\left(x=t\wedge \phi \right)\leftrightarrow \left(x=t\wedge \psi \right)$$
3	2	exbii	$$⊢\exists x\left(x=t\wedge \phi \right)\leftrightarrow \exists x\left(x=t\wedge \psi \right)$$
4		19.41v	$$⊢\exists x\left(x=t\wedge \psi \right)\leftrightarrow \left(\exists xx=t\wedge \psi \right)$$
5	3 4	bitri	$$⊢\exists x\left(x=t\wedge \phi \right)\leftrightarrow \left(\exists xx=t\wedge \psi \right)$$
6	1	biimprcd	$$⊢\psi \to \left(x=t\to \phi \right)$$
7	6	alrimiv	$$⊢\psi \to \forall x\left(x=t\to \phi \right)$$
8	5 7	simplbiim	$$⊢\exists x\left(x=t\wedge \phi \right)\to \forall x\left(x=t\to \phi \right)$$