Theorem 19.42v 1906

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

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1909  19.42vv  1911  19.42vvv  1912  4exdistr  1916  cbvex2  1922  2sb5  1983  2sb5rf  1989  rexcom4a  2761  ceqsex2  2777  reuind  2942  2rmorex  2943  sbccomlem  3037  bm1.3ii  4124  opm  4234  eqvinop  4243  uniuni  4451  elco  4793  dmopabss  4839  dmopab3  4840  mptpreima  5122  brprcneu  5508  relelfvdm  5547  fndmin  5623  fliftf  5799  dfoprab2  5921  dmoprab  5955  dmoprabss  5956  fnoprabg  5975  opabex3d  6121  opabex3  6122  eroveu  6625  dmaddpq  7377  dmmulpq  7378  prarloc  7501  ltexprlemopl  7599  ltexprlemlol  7600  ltexprlemopu  7601  ltexprlemupu  7602  shftdm  10826  ntreq0  13563  bdbm1.3ii  14563