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  2762  ceqsex2  2778  reuind  2943  2rmorex  2944  sbccomlem  3038  bm1.3ii  4125  opm  4235  eqvinop  4244  uniuni  4452  elco  4794  dmopabss  4840  dmopab3  4841  mptpreima  5123  brprcneu  5509  relelfvdm  5548  fndmin  5624  fliftf  5800  dfoprab2  5922  dmoprab  5956  dmoprabss  5957  fnoprabg  5976  opabex3d  6122  opabex3  6123  eroveu  6626  dmaddpq  7378  dmmulpq  7379  prarloc  7502  ltexprlemopl  7600  ltexprlemlol  7601  ltexprlemopu  7602  ltexprlemupu  7603  shftdm  10831  ntreq0  13635  bdbm1.3ii  14646