Theorem eeanv 1318

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 1304	. 2 |- (E.xE.y(ph /\ ps) <-> E.x(ph /\ E.yps))
2		ax-17 968	. . . 4 |- (ps -> A.xps)
3	2	hbex 1003	. . 3 |- (E.yps -> A.xE.yps)
4	3	19.41 1091	. 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 977

This theorem is referenced by:  eeeanv 1319  ee4anv 1320  2eu4 1445  reeanv 1770  cgsex2g 1823  cgsex4g 1824  vtocl2 1834  cla42egv 1855  csbie2t 2023  dtruALT 2738  copsex2g 2783  xpnz 3452  fununi 3549  tfrlem7 3902  ener 4391  domtr 4396  unen 4414  sbthlem10 4436  abfii4 4538  aceq5lem4 4710  zorn2lem6 4765  genpn0 5078  genpnnp 5080  mulgt0sr 5186  uzindOLD 6156  creur 6673  creui 6674  replimt 6692  subbas 7586

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975

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

Copyright terms: Public domain