Theorem 19.41 1957

Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1757 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.)

Hypothesis

Ref	Expression
19.41.1	|- F/ x ps

Assertion

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

Proof of Theorem 19.41

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

Syntax hints:   <-> wb 184   /\ wa 369   E.wex 1599   F/wnf 1603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-12 1840

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-nf 1604

This theorem is referenced by:  19.42  1958  exan  1959  eean  1973  eeeanv  1975  2sb5rf  2181  r19.41  2996  eliunxp  5130  dfopab2  6839  dfoprab3s  6840  xpcomco  7609  mpt2mptxf  27496  eliunxp2  32791  2sb5nd  33201  2sb5ndVD  33578  2sb5ndALT  33600  bnj605  33833  bnj607  33842