Theorem 19.42v 1886

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

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

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exdistr  1889  19.42vv  1891  19.42vvv  1892  4exdistr  1896  cbvex2  1902  2sb5  1963  2sb5rf  1969  rexcom4a  2736  ceqsex2  2752  reuind  2917  2rmorex  2918  sbccomlem  3011  bm1.3ii  4085  opm  4194  eqvinop  4203  uniuni  4411  elco  4752  dmopabss  4798  dmopab3  4799  mptpreima  5079  brprcneu  5461  relelfvdm  5500  fndmin  5574  fliftf  5749  dfoprab2  5868  dmoprab  5902  dmoprabss  5903  fnoprabg  5922  opabex3d  6069  opabex3  6070  eroveu  6571  dmaddpq  7299  dmmulpq  7300  prarloc  7423  ltexprlemopl  7521  ltexprlemlol  7522  ltexprlemopu  7523  ltexprlemupu  7524  shftdm  10722  ntreq0  12532  bdbm1.3ii  13466