Theorem 19.42v 1918

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1921  19.42vv  1923  19.42vvv  1924  4exdistr  1928  cbvex2  1934  2sb5  1999  2sb5rf  2005  rexcom4a  2784  ceqsex2  2801  reuind  2966  2rmorex  2967  sbccomlem  3061  bm1.3ii  4151  opm  4264  eqvinop  4273  uniuni  4483  elco  4829  dmopabss  4875  dmopab3  4876  mptpreima  5160  brprcneu  5548  relelfvdm  5587  fndmin  5666  fliftf  5843  dfoprab2  5966  dmoprab  6000  dmoprabss  6001  fnoprabg  6020  opabex3d  6175  opabex3  6176  eroveu  6682  dmaddpq  7441  dmmulpq  7442  prarloc  7565  ltexprlemopl  7663  ltexprlemlol  7664  ltexprlemopu  7665  ltexprlemupu  7666  shftdm  10969  fngsum  12974  igsumvalx  12975  ntreq0  14311  bdbm1.3ii  15453