Theorem 19.41

Description: Theorem 19.41 of Margaris p. 90. See 19.41v for a version requiring fewer axioms. (Contributed by NM, 14-May-1993) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 12-Jan-2018)

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

Proof

Step	Hyp	Ref	Expression
1		19.41.1	|- F/ x ps
2		19.40	|- ( E. x ( ph /\ ps ) -> ( E. x ph /\ E. x ps ) )
3	1	19.9	|- ( E. x ps <-> ps )
4	3	anbi2i	|- ( ( E. x ph /\ E. x ps ) <-> ( E. x ph /\ ps ) )
5	2 4	sylib	|- ( E. x ( ph /\ ps ) -> ( E. x ph /\ ps ) )
6		pm3.21	|- ( ps -> ( ph -> ( ph /\ ps ) ) )
7	1 6	eximd	|- ( ps -> ( E. x ph -> E. x ( ph /\ ps ) ) )
8	7	impcom	|- ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) )
9	5 8	impbii	|- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )