Theorem eeanv 1323

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 1309	. 2 |- (E.xE.y(ph /\ ps) <-> E.x(ph /\ E.yps))
2		ax-17 971	. . . 4 |- (ps -> A.xps)
3	2	hbex 1006	. . 3 |- (E.yps -> A.xE.yps)
4	3	19.41 1095	. 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 980

This theorem is referenced by:  eeeanv 1324  ee4anv 1325  2eu4 1452  reeanv 1777  cgsex2g 1830  cgsex4g 1831  vtocl2 1841  cla42egv 1862  csbie2t 2031  dtruALT 2746  copsex2g 2791  xpnz 3464  fununi 3561  tfrlem7 3915  ener 4405  domtr 4410  unen 4428  sbthlem10 4450  abfii4 4552  aceq5lem4 4726  zorn2lem6 4781  genpn0 5094  genpnnp 5096  mulgt0sr 5202  uzindOLD 6176  creur 6702  creui 6703  replimt 6721  subbas 7601

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

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

Copyright terms: Public domain