Theorem 19.42v 1921

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistr  1924  19.42vv  1926  19.42vvv  1927  4exdistr  1931  cbvex2  1937  2sb5  2002  2sb5rf  2008  rexcom4a  2787  ceqsex2  2804  reuind  2969  2rmorex  2970  sbccomlem  3064  bm1.3ii  4155  opm  4268  eqvinop  4277  uniuni  4487  elco  4833  dmopabss  4879  dmopab3  4880  mptpreima  5164  brprcneu  5554  relelfvdm  5593  fndmin  5672  fliftf  5849  dfoprab2  5973  dmoprab  6007  dmoprabss  6008  fnoprabg  6027  opabex3d  6187  opabex3  6188  eroveu  6694  dmaddpq  7463  dmmulpq  7464  prarloc  7587  ltexprlemopl  7685  ltexprlemlol  7686  ltexprlemopu  7687  ltexprlemupu  7688  shftdm  11004  fngsum  13090  igsumvalx  13091  ntreq0  14452  bdbm1.3ii  15621