ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  reeanv Unicode version

Theorem reeanv 2577
Description: Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.)
Assertion
Ref Expression
reeanv  |-  ( E. x  e.  A  E. y  e.  B  ( ph  /\  ps )  <->  ( E. x  e.  A  ph  /\  E. y  e.  B  ps ) )
Distinct variable groups:    ph, y    ps, x    x, y    y, A   
x, B
Allowed substitution hints:    ph( x)    ps( y)    A( x)    B( y)

Proof of Theorem reeanv
StepHypRef Expression
1 nfv 1493 . 2  |-  F/ y
ph
2 nfv 1493 . 2  |-  F/ x ps
31, 2reean 2576 1  |-  ( E. x  e.  A  E. y  e.  B  ( ph  /\  ps )  <->  ( E. x  e.  A  ph  /\  E. y  e.  B  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104   E.wrex 2394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399
This theorem is referenced by:  3reeanv  2578  fliftfun  5665  tfrlem5  6179  eroveu  6488  erovlem  6489  xpf1o  6706  genprndl  7297  genprndu  7298  ltpopr  7371  ltsopr  7372  cauappcvgprlemdisj  7427  caucvgprlemdisj  7450  caucvgprprlemdisj  7478  exbtwnzlemex  9995  rebtwn2z  10000  rexanre  10960  summodc  11120  dvds2lem  11432  odd2np1  11497  opoe  11519  omoe  11520  opeo  11521  omeo  11522  gcddiv  11634  divgcdcoprmex  11710  tgcl  12160  restbasg  12264  txuni2  12352  txbas  12354  txcnp  12367  blin2  12528  tgqioo  12643
  Copyright terms: Public domain W3C validator