Theorem 19.42v 1942

Description: Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 21-Jun-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		nfv 1678	. 2 |- F/ x ph
2	1	19.42 1916	1 |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )

Syntax hints:   <-> wb 184   /\ wa 369   E.wex 1591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-12 1798

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595

This theorem is referenced by:  exdistr  1943  19.42vv  1944  19.42vvv  1945  4exdistr  1948  eeeanv  1951  cbvex2OLD  1995  2sb5  2164  2sb5rfOLD  2176  rexcom4a  3127  ceqsex2  3144  reuind  3300  2reu5lem3  3304  sbccomlem  3403  bm1.3ii  4564  eqvinop  4724  dmopabss  5205  dmopab3  5206  mptpreima  5491  brprcneu  5850  fndmin  5979  fliftf  6192  dfoprab2  6318  dmoprab  6358  dmoprabss  6359  fnoprabg  6378  uniuni  6580  zfrep6  6742  opabex3d  6752  opabex3  6753  fsplit  6878  eroveu  7396  rankuni  8270  aceq1  8487  dfac3  8491  kmlem14  8532  kmlem15  8533  axdc2lem  8817  1idpr  9396  ltexprlem1  9403  ltexprlem4  9406  shftdm  12854  joindm  15479  meetdm  15493  ntreq0  19337  cnextf  20294  usg2spot2nb  24728  adjeu  26470  rexunirn  27052  mptfnf  27157  fpwrelmapffslem  27213  dfiota3  29136  brimg  29150  funpartlem  29155  itg2addnc  29633  sbccom2lem  30120  pm11.58  30829  pm11.71  30836  2sbc5g  30856  iotasbc2  30860  stoweidlem60  31315  ax6e2nd  32286  ax6e2ndVD  32663  ax6e2ndALT  32685  bnj1019  32792  bnj1209  32809  bnj1033  32979  bnj1189  33019  bj-eeanvw  33224  bj-rexcom4  33401  bj-rexcom4a  33402  bj-snsetex  33477  bj-snglc  33483  xpcogend  36658