Theorem 19.41 2062

Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1841 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 1742	. . 3 |- ( E. x ( ph /\ ps ) -> ( E. x ph /\ E. x ps ) )
2		19.41.1	. . . . 5 |- F/ x ps
3	2	19.9 1981	. . . 4 |- ( E. x ps <-> ps )
4	3	anbi2i 705	. . 3 |- ( ( E. x ph /\ E. x ps ) <-> ( E. x ph /\ ps ) )
5	1, 4	sylib 201	. 2 |- ( E. x ( ph /\ ps ) -> ( E. x ph /\ ps ) )
6		pm3.21 454	. . . 4 |- ( ps -> ( ph -> ( ph /\ ps ) ) )
7	2, 6	eximd 1971	. . 3 |- ( ps -> ( E. x ph -> E. x ( ph /\ ps ) ) )
8	7	impcom 436	. 2 |- ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) )
9	5, 8	impbii 192	1 |- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )

Syntax hints:   <-> wb 189   /\ wa 375   E.wex 1674   F/wnf 1678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679

This theorem is referenced by:  19.42  2063  exan  2064  equsexv  2077  eean  2088  eeeanv  2090  equsexALT  2142  2sb5rf  2291  r19.41  2955  eliunxp  4991  dfopab2  6874  dfoprab3s  6875  xpcomco  7688  mpt2mptxf  28329  bnj605  29767  bnj607  29776  2sb5nd  36971  2sb5ndVD  37347  2sb5ndALT  37369  eliunxp2  40388