Theorem 19.42v 1931

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1934  19.42vv  1936  19.42vvv  1937  4exdistr  1941  cbvex2  1947  2sb5  2012  2sb5rf  2018  rexcom4a  2798  ceqsex2  2815  reuind  2982  2rmorex  2983  sbccomlem  3077  bm1.3ii  4173  opm  4286  eqvinop  4295  uniuni  4506  elco  4852  dmopabss  4899  dmopab3  4900  mptpreima  5185  brprcneu  5582  relelfvdm  5621  fndmin  5700  fliftf  5881  dfoprab2  6005  dmoprab  6039  dmoprabss  6040  fnoprabg  6059  opabex3d  6219  opabex3  6220  eroveu  6726  dmaddpq  7512  dmmulpq  7513  prarloc  7636  ltexprlemopl  7734  ltexprlemlol  7735  ltexprlemopu  7736  ltexprlemupu  7737  shftdm  11208  fngsum  13295  igsumvalx  13296  ntreq0  14679  bdbm1.3ii  15965