Theorem 19.42v 1955

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 1574	. 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 1540

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1958  19.42vv  1960  19.42vvv  1961  4exdistr  1965  cbvex2  1971  2sb5  2036  2sb5rf  2042  rexcom4a  2827  ceqsex2  2844  reuind  3011  2rmorex  3012  sbccomlem  3106  bm1.3ii  4210  opm  4326  eqvinop  4335  uniuni  4548  elco  4896  dmopabss  4943  dmopab3  4944  mptpreima  5230  brprcneu  5632  relelfvdm  5671  fndmin  5754  fliftf  5940  dfoprab2  6068  dmoprab  6102  dmoprabss  6103  fnoprabg  6122  opabex3d  6283  opabex3  6284  eroveu  6795  dmaddpq  7599  dmmulpq  7600  prarloc  7723  ltexprlemopl  7821  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  shftdm  11400  fngsum  13489  igsumvalx  13490  ntreq0  14875  bdbm1.3ii  16537