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

Theorem reeanv 2528
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 1462 . 2  |-  F/ y
ph
2 nfv 1462 . 2  |-  F/ x ps
31, 2reean 2527 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 102    <-> wb 103   E.wrex 2354
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359
This theorem is referenced by:  3reeanv  2529  fliftfun  5487  tfrlem5  5983  eroveu  6284  erovlem  6285  xpf1o  6406  genprndl  6825  genprndu  6826  ltpopr  6899  ltsopr  6900  cauappcvgprlemdisj  6955  caucvgprlemdisj  6978  caucvgprprlemdisj  7006  exbtwnzlemex  9388  rebtwn2z  9393  rexanre  10307  dvds2lem  10415  odd2np1  10480  opoe  10502  omoe  10503  opeo  10504  omeo  10505  gcddiv  10615  divgcdcoprmex  10691
  Copyright terms: Public domain W3C validator