Theorem 19.41 1979

Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1779 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 1687	. . 3 |- ( E. x ( ph /\ ps ) -> ( E. x ph /\ E. x ps ) )
2		19.41.1	. . . . 5 |- F/ x ps
3	2	19.9 1901	. . . 4 |- ( E. x ps <-> ps )
4	3	anbi2i 692	. . 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 446	. . . 4 |- ( ps -> ( ph -> ( ph /\ ps ) ) )
7	2, 6	eximd 1890	. . 3 |- ( ps -> ( E. x ph -> E. x ( ph /\ ps ) ) )
8	7	impcom 428	. 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 367   E.wex 1620   F/wnf 1624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-12 1862

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-nf 1625

This theorem is referenced by:  19.42  1980  exan  1981  eean  1995  eeeanv  1997  2sb5rf  2199  r19.41  2935  eliunxp  5053  dfopab2  6753  dfoprab3s  6754  xpcomco  7526  mpt2mptxf  27665  eliunxp2  33123  2sb5nd  33673  2sb5ndVD  34057  2sb5ndALT  34079  bnj605  34312  bnj607  34321