Theorem 19.42v 1845

Description: Version of 19.42 2063 with a dv condition requiring fewer axioms. (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		19.41v 1841	. 2 |- ( E. x ( ps /\ ph ) <-> ( E. x ps /\ ph ) )
2		exancom 1733	. 2 |- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )
3		ancom 456	. 2 |- ( ( ph /\ E. x ps ) <-> ( E. x ps /\ ph ) )
4	1, 2, 3	3bitr4i 285	1 |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )

Syntax hints:   <-> wb 189   /\ wa 375   E.wex 1674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675

This theorem is referenced by:  exdistr  1846  19.42vv  1847  19.42vvv  1848  4exdistr  1851  eeeanv  2090  2sb5  2283  rexcom4a  3080  ceqsex2  3098  reuind  3255  2reu5lem3  3259  sbccomlem  3350  bm1.3ii  4544  eqvinop  4703  dmopabss  5068  dmopab3  5069  mptpreima  5351  mptfnf  5725  brprcneu  5885  fndmin  6017  fliftf  6238  dfoprab2  6369  dmoprab  6409  dmoprabss  6410  fnoprabg  6429  uniuni  6632  zfrep6  6793  opabex3d  6803  opabex3  6804  fsplit  6933  eroveu  7489  rankuni  8365  aceq1  8579  dfac3  8583  kmlem14  8624  kmlem15  8625  axdc2lem  8909  1idpr  9485  ltexprlem1  9492  ltexprlem4  9495  xpcogend  13093  shftdm  13189  joindm  16304  meetdm  16318  ntreq0  20148  cnextf  21136  usg2spot2nb  25849  adjeu  27598  rexunirn  28183  fpwrelmapffslem  28369  bnj1019  29641  bnj1209  29658  bnj1033  29828  bnj1189  29868  dfiota3  30740  brimg  30754  funpartlem  30759  bj-eeanvw  31353  bj-rexcom4  31524  bj-rexcom4a  31525  bj-snsetex  31603  bj-snglc  31609  itg2addnc  32042  sbccom2lem  32410  rp-isfinite6  36209  undmrnresiss  36256  elintima  36291  pm11.58  36785  pm11.71  36792  2sbc5g  36812  iotasbc2  36816  ax6e2nd  36970  ax6e2ndVD  37346  ax6e2ndALT  37368  stoweidlem60  38022