Theorem eeanv 1321

Description: Rearrange existential quantifiers.

Assertion

Ref	Expression
eeanv	|- (E.xE.y(ph /\ ps) <-> (E.xph /\ E.yps))

Distinct variable groups:   ph,y   ps,x

Proof of Theorem eeanv

Step	Hyp	Ref	Expression
1		exdistr 1307	. 2 |- (E.xE.y(ph /\ ps) <-> E.x(ph /\ E.yps))
2		ax-17 969	. . . 4 |- (ps -> A.xps)
3	2	hbex 1004	. . 3 |- (E.yps -> A.xE.yps)
4	3	19.41 1093	. 2 |- (E.x(ph /\ E.yps) <-> (E.xph /\ E.yps))
5	1, 4	bitr 173	1 |- (E.xE.y(ph /\ ps) <-> (E.xph /\ E.yps))

Syntax hints:   <-> wb 146   /\ wa 223  E.wex 978

This theorem is referenced by:  eeeanv 1322  ee4anv 1323  2eu4 1450  reeanv 1775  cgsex2g 1828  cgsex4g 1829  vtocl2 1839  cla42egv 1860  csbie2t 2029  dtruALT 2743  copsex2g 2788  xpnz 3458  fununi 3555  tfrlem7 3908  ener 4397  domtr 4402  unen 4420  sbthlem10 4442  abfii4 4544  aceq5lem4 4718  zorn2lem6 4773  genpn0 5086  genpnnp 5088  mulgt0sr 5194  uzindOLD 6164  creur 6681  creui 6682  replimt 6700  subbas 7594

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979

Copyright terms: Public domain