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 -> ( ph <-> ps ) )
Assertion	bj-substw	|- ( E. x ( x = t /\ ph ) -> A. x ( x = t -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		bj-substw.is	|- ( x = t -> ( ph <-> ps ) )
2	1	pm5.32i	|- ( ( x = t /\ ph ) <-> ( x = t /\ ps ) )
3	2	exbii	|- ( E. x ( x = t /\ ph ) <-> E. x ( x = t /\ ps ) )
4		19.41v	|- ( E. x ( x = t /\ ps ) <-> ( E. x x = t /\ ps ) )
5	3 4	bitri	|- ( E. x ( x = t /\ ph ) <-> ( E. x x = t /\ ps ) )
6	1	biimprcd	|- ( ps -> ( x = t -> ph ) )
7	6	alrimiv	|- ( ps -> A. x ( x = t -> ph ) )
8	5 7	simplbiim	|- ( E. x ( x = t /\ ph ) -> A. x ( x = t -> ph ) )