MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reeanv Structured version   Unicode version

Theorem reeanv 2996
Description: Rearrange restricted 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 1751 . 2  |-  F/ y
ph
2 nfv 1751 . 2  |-  F/ x ps
31, 2reean 2995 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 setvar class
Syntax hints:    <-> wb 187    /\ wa 370   E.wrex 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664  df-ral 2780  df-rex 2781
This theorem is referenced by:  3reeanv  2997  2ralor  2998  disjxiun  4417  fliftfun  6216  tfrlem5  7102  uniinqs  7447  eroveu  7462  erovlem  7463  xpf1o  7736  unxpdomlem3  7780  unfi  7840  finsschain  7883  dffi3  7947  rankxplim3  8353  xpnum  8386  kmlem9  8588  sornom  8707  fpwwe2lem12  9066  cnegex  9814  zaddcl  10977  rexanre  13397  o1lo1  13588  o1co  13637  rlimcn2  13641  o1of2  13663  lo1add  13677  lo1mul  13678  summo  13770  ntrivcvgmul  13945  prodmolem2  13976  prodmo  13977  dvds2lem  14302  odd2np1  14352  bezoutlem4OLD  14493  bezoutlem4  14496  gcddiv  14504  opoe  14748  omoe  14749  opeo  14750  omeo  14751  pcqmul  14790  pcadd  14821  mul4sq  14885  4sqlem12  14887  prmgaplem7  15014  gaorber  16949  psgneu  17134  lsmsubm  17292  pj1eu  17333  efgredlem  17384  efgrelexlemb  17387  qusabl  17490  cygabl  17512  dprdsubg  17644  dvdsrtr  17867  unitgrp  17882  lss1d  18173  lsmspsn  18294  lspsolvlem  18352  lbsextlem2  18369  znfld  19117  cygznlem3  19126  psgnghm  19134  tgcl  19971  restbas  20160  ordtbas2  20193  uncmp  20404  txuni2  20566  txbas  20568  ptbasin  20578  txcnp  20621  txlly  20637  txnlly  20638  tx1stc  20651  tx2ndc  20652  fbasrn  20885  rnelfmlem  20953  fmfnfmlem3  20957  txflf  21007  qustgplem  21121  trust  21230  utoptop  21235  fmucndlem  21292  blin2  21430  metustto  21554  tgqioo  21804  minveclem3b  22356  minveclem3bOLD  22368  pmltpc  22387  evthicc2  22397  ovolunlem2  22437  dyaddisj  22540  rolle  22928  dvcvx  22958  itgsubst  22987  plyadd  23157  plymul  23158  coeeu  23165  aalioulem6  23279  dchrptlem2  24179  lgsdchr  24262  mul2sq  24279  2sqlem5  24282  pntibnd  24417  pntlemp  24434  cgraswap  24848  cgracom  24850  cgratr  24851  dfcgra2  24857  acopyeu  24861  ax5seg  24954  axpasch  24957  axeuclid  24979  axcontlem4  24983  axcontlem9  24988  usgra2edg  25095  frgrawopreglem5  25761  pjhthmo  26940  superpos  27992  chirredi  28032  cdjreui  28070  cdj3i  28079  xrofsup  28346  archiabllem2c  28506  ordtconlem1  28725  dya2iocnrect  29098  txpcon  29950  cvmlift2lem10  30030  cvmlift3lem7  30043  msubco  30164  mclsppslem  30216  ghomgrpilem2  30299  poseq  30485  soseq  30486  altopelaltxp  30735  funtransport  30790  btwnconn1lem13  30858  btwnconn1lem14  30859  segletr  30873  segleantisym  30874  funray  30899  funline  30901  tailfb  31025  mblfinlem3  31892  ismblfin  31894  itg2addnc  31909  ftc1anclem6  31935  heibor1lem  32054  crngohomfo  32152  ispridlc  32216  prter1  32368  hl2at  32888  cdlemn11pre  34696  dihord2pre  34711  dihord4  34744  dihmeetlem20N  34812  mapdpglem32  35191  diophin  35533  diophun  35534  iunrelexpuztr  36170  mullimc  37515  mullimcf  37522  addlimc  37548  fourierdlem42  37831  fourierdlem42OLD  37832  fourierdlem80  37869  sge0resplit  38035  2reu4a  38322  usgr2edg  38913
  Copyright terms: Public domain W3C validator