Theorem 19.42v 1958

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  1961  19.42vv  1963  19.42vvv  1964  4exdistr  1968  cbvex2  1974  2sb5  2039  2sb5rf  2045  rexcom4a  2840  ceqsex2  2857  reuind  3025  2rmorex  3026  sbccomlem  3120  bm1.3ii  4236  opm  4355  eqvinop  4364  uniuni  4577  elco  4926  dmopabss  4973  dmopab3  4974  mptpreima  5261  brprcneu  5668  relelfvdm  5707  fndmin  5790  fliftf  5978  dfoprab2  6108  dmoprab  6142  dmoprabss  6143  fnoprabg  6162  opabex3d  6323  opabex3  6324  eroveu  6873  dmaddpq  7710  dmmulpq  7711  prarloc  7834  ltexprlemopl  7932  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  shftdm  11532  fngsum  13651  igsumvalx  13652  ntreq0  15123  bdbm1.3ii  16787