Theorem 19.42v 1956

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 1575	. 2 |- ( ph -> A. x ph )
2	1	19.42h 1735	1 |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1959  19.42vv  1961  19.42vvv  1962  4exdistr  1966  cbvex2  1972  2sb5  2037  2sb5rf  2043  rexcom4a  2837  ceqsex2  2854  reuind  3021  2rmorex  3022  sbccomlem  3116  bm1.3ii  4230  opm  4349  eqvinop  4358  uniuni  4571  elco  4920  dmopabss  4967  dmopab3  4968  mptpreima  5255  brprcneu  5662  relelfvdm  5701  fndmin  5784  fliftf  5971  dfoprab2  6099  dmoprab  6133  dmoprabss  6134  fnoprabg  6153  opabex3d  6313  opabex3  6314  eroveu  6859  dmaddpq  7693  dmmulpq  7694  prarloc  7817  ltexprlemopl  7915  ltexprlemlol  7916  ltexprlemopu  7917  ltexprlemupu  7918  shftdm  11503  fngsum  13593  igsumvalx  13594  ntreq0  14989  bdbm1.3ii  16653