Theorem 19.23v

Description: Version of 19.23 with a disjoint variable condition instead of a non-freeness hypothesis. (Contributed by NM, 28-Jun-1998) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020) Remove dependency on ax-6 . (Revised by Rohan Ridenour, 15-Apr-2022)

	Ref	Expression
Assertion	19.23v	|- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		exim	|- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
2		ax5e	|- ( E. x ps -> ps )
3	1 2	syl6	|- ( A. x ( ph -> ps ) -> ( E. x ph -> ps ) )
4		ax-5	|- ( ps -> A. x ps )
5	4	imim2i	|- ( ( E. x ph -> ps ) -> ( E. x ph -> A. x ps ) )
6		19.38	|- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
7	5 6	syl	|- ( ( E. x ph -> ps ) -> A. x ( ph -> ps ) )
8	3 7	impbii	|- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )