Theorem 19.42v 1936

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 1674	. 2 |- F/ x ph
2	1	19.42 1912	1 |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591

This theorem is referenced by:  exdistr  1937  19.42vv  1938  19.42vvv  1939  4exdistr  1942  eeeanv  1945  cbvex2OLD  1989  2sb5  2158  2sb5rfOLD  2170  rexcom4a  3099  ceqsex2  3116  reuind  3270  2reu5lem3  3274  sbccomlem  3373  bm1.3ii  4525  eqvinop  4684  dmopabss  5160  dmopab3  5161  mptpreima  5440  brprcneu  5793  fndmin  5920  fliftf  6118  dfoprab2  6243  dmoprab  6282  dmoprabss  6283  fnoprabg  6302  uniuni  6496  zfrep6  6656  opabex3d  6666  opabex3  6667  fsplit  6788  eroveu  7306  rankuni  8182  aceq1  8399  dfac3  8403  kmlem14  8444  kmlem15  8445  axdc2lem  8729  1idpr  9310  ltexprlem1  9317  ltexprlem4  9320  shftdm  12679  joindm  15293  meetdm  15307  ntreq0  18814  cnextf  19771  adjeu  25446  rexunirn  26028  mptfnf  26128  fpwrelmapffslem  26184  dfiota3  28099  brimg  28113  funpartlem  28118  itg2addnc  28595  sbccom2lem  29082  pm11.58  29792  pm11.71  29799  2sbc5g  29819  iotasbc2  29823  stoweidlem60  30004  usg2spot2nb  30807  ax6e2nd  31600  ax6e2ndVD  31977  ax6e2ndALT  31999  bnj1019  32106  bnj1209  32123  bnj1033  32293  bnj1189  32333  bj-eeanvw  32536  bj-rexcom4  32713  bj-rexcom4a  32714  bj-snsetex  32789  bj-snglc  32795