Theorem 19.42v 1918

Description: Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Distinct variable group:   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem 19.42v

Step	Hyp	Ref	Expression
1		ax-17 1537	. 2 |- ( ph -> A. x ph )
2	1	19.42h 1698	1 |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )

Syntax hints:   /\ wa 104   <-> wb 105   E.wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1921  19.42vv  1923  19.42vvv  1924  4exdistr  1928  cbvex2  1934  2sb5  1999  2sb5rf  2005  rexcom4a  2784  ceqsex2  2800  reuind  2965  2rmorex  2966  sbccomlem  3060  bm1.3ii  4150  opm  4263  eqvinop  4272  uniuni  4482  elco  4828  dmopabss  4874  dmopab3  4875  mptpreima  5159  brprcneu  5547  relelfvdm  5586  fndmin  5665  fliftf  5842  dfoprab2  5965  dmoprab  5999  dmoprabss  6000  fnoprabg  6019  opabex3d  6173  opabex3  6174  eroveu  6680  dmaddpq  7439  dmmulpq  7440  prarloc  7563  ltexprlemopl  7661  ltexprlemlol  7662  ltexprlemopu  7663  ltexprlemupu  7664  shftdm  10966  fngsum  12971  igsumvalx  12972  ntreq0  14300  bdbm1.3ii  15383