Theorem 19.42v 1879

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

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

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exdistr  1882  19.42vv  1884  19.42vvv  1885  4exdistr  1889  cbvex2  1895  2sb5  1959  2sb5rf  1965  rexcom4a  2713  ceqsex2  2729  reuind  2893  2rmorex  2894  sbccomlem  2987  bm1.3ii  4057  opm  4164  eqvinop  4173  uniuni  4380  elco  4713  dmopabss  4759  dmopab3  4760  mptpreima  5040  brprcneu  5422  relelfvdm  5461  fndmin  5535  fliftf  5708  dfoprab2  5826  dmoprab  5860  dmoprabss  5861  fnoprabg  5880  opabex3d  6027  opabex3  6028  eroveu  6528  dmaddpq  7211  dmmulpq  7212  prarloc  7335  ltexprlemopl  7433  ltexprlemlol  7434  ltexprlemopu  7435  ltexprlemupu  7436  shftdm  10626  ntreq0  12340  bdbm1.3ii  13260