Theorem 19.42v 1783

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.xps))

Distinct variable group:   ph,x

Allowed substitution hint:   ps(x)

Proof of Theorem 19.42v

Step	Hyp	Ref	Expression
1		ax-17 1416	. 2 |- (ph -> A.xph)
2	1	19.42h 1574	1 |- (E.x(ph /\ ps) <-> (ph /\ E.xps))

Syntax hints:   /\ wa 97   <-> wb 98  E.wex 1378

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  exdistr  1784  19.42vv  1785  19.42vvv  1786  4exdistr  1790  cbvex2  1794  2sb5  1856  2sb5rf  1862  rexcom4a  2572  ceqsex2  2588  reuind  2738  2rmorex  2739  sbccomlem  2826  bm1.3ii  3869  opm  3962  eqvinop  3971  uniuni  4149  dmopabss  4490  dmopab3  4491  mptpreima  4757  brprcneu  5114  relelfvdm  5148  fndmin  5217  fliftf  5382  dfoprab2  5494  dmoprab  5527  dmoprabss  5528  fnoprabg  5544  opabex3d  5690  opabex3  5691  eroveu  6133  dmaddpq  6363  dmmulpq  6364  prarloc  6486  ltexprlemopl  6575  ltexprlemlol  6576  ltexprlemopu  6577  ltexprlemupu  6578  bdbm1.3ii  9346