Theorem 19.42v 1894

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

Syntax hints:   /\ wa 103   <-> wb 104   E.wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exdistr  1897  19.42vv  1899  19.42vvv  1900  4exdistr  1904  cbvex2  1910  2sb5  1971  2sb5rf  1977  rexcom4a  2750  ceqsex2  2766  reuind  2931  2rmorex  2932  sbccomlem  3025  bm1.3ii  4103  opm  4212  eqvinop  4221  uniuni  4429  elco  4770  dmopabss  4816  dmopab3  4817  mptpreima  5097  brprcneu  5479  relelfvdm  5518  fndmin  5592  fliftf  5767  dfoprab2  5889  dmoprab  5923  dmoprabss  5924  fnoprabg  5943  opabex3d  6089  opabex3  6090  eroveu  6592  dmaddpq  7320  dmmulpq  7321  prarloc  7444  ltexprlemopl  7542  ltexprlemlol  7543  ltexprlemopu  7544  ltexprlemupu  7545  shftdm  10764  ntreq0  12772  bdbm1.3ii  13773