Theorem 19.42v 1930

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1933  19.42vv  1935  19.42vvv  1936  4exdistr  1940  cbvex2  1946  2sb5  2011  2sb5rf  2017  rexcom4a  2796  ceqsex2  2813  reuind  2978  2rmorex  2979  sbccomlem  3073  bm1.3ii  4166  opm  4279  eqvinop  4288  uniuni  4499  elco  4845  dmopabss  4891  dmopab3  4892  mptpreima  5177  brprcneu  5571  relelfvdm  5610  fndmin  5689  fliftf  5870  dfoprab2  5994  dmoprab  6028  dmoprabss  6029  fnoprabg  6048  opabex3d  6208  opabex3  6209  eroveu  6715  dmaddpq  7494  dmmulpq  7495  prarloc  7618  ltexprlemopl  7716  ltexprlemlol  7717  ltexprlemopu  7718  ltexprlemupu  7719  shftdm  11166  fngsum  13253  igsumvalx  13254  ntreq0  14637  bdbm1.3ii  15864