Theorem 19.42v 1953

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1956  19.42vv  1958  19.42vvv  1959  4exdistr  1963  cbvex2  1969  2sb5  2034  2sb5rf  2040  rexcom4a  2824  ceqsex2  2841  reuind  3008  2rmorex  3009  sbccomlem  3103  bm1.3ii  4205  opm  4320  eqvinop  4329  uniuni  4542  elco  4888  dmopabss  4935  dmopab3  4936  mptpreima  5222  brprcneu  5620  relelfvdm  5659  fndmin  5742  fliftf  5923  dfoprab2  6051  dmoprab  6085  dmoprabss  6086  fnoprabg  6105  opabex3d  6266  opabex3  6267  eroveu  6773  dmaddpq  7566  dmmulpq  7567  prarloc  7690  ltexprlemopl  7788  ltexprlemlol  7789  ltexprlemopu  7790  ltexprlemupu  7791  shftdm  11333  fngsum  13421  igsumvalx  13422  ntreq0  14806  bdbm1.3ii  16254