Theorem 19.41v

Description: Version of 19.41 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993) Remove dependency on ax-6 . (Revised by Rohan Ridenour, 15-Apr-2022)

	Ref	Expression
Assertion	19.41v	|- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		19.40	|- ( E. x ( ph /\ ps ) -> ( E. x ph /\ E. x ps ) )
2		ax5e	|- ( E. x ps -> ps )
3	2	anim2i	|- ( ( E. x ph /\ E. x ps ) -> ( E. x ph /\ ps ) )
4	1 3	syl	|- ( E. x ( ph /\ ps ) -> ( E. x ph /\ ps ) )
5		pm3.21	|- ( ps -> ( ph -> ( ph /\ ps ) ) )
6	5	eximdv	|- ( ps -> ( E. x ph -> E. x ( ph /\ ps ) ) )
7	6	impcom	|- ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) )
8	4 7	impbii	|- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )