Theorem reeanv 3317

Description: Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999.)

Assertion

Ref	Expression
reeanv	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝑦   𝑦,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem reeanv

Step	Hyp	Ref	Expression
1		nfv 2013	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 2013	. 2 ⊢ Ⅎ𝑥𝜓
3	1, 2	reean 3316	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ↔ wb 198   ∧ wa 386  ∃wrex 3118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-10 2192  ax-11 2207  ax-12 2220

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-ral 3122  df-rex 3123

This theorem is referenced by:  3reeanv  3318  2ralor  3319  disjxiun  4872  fliftfun  6822  tfrlem5  7747  uniinqs  8097  eroveu  8113  erovlem  8114  xpf1o  8397  unxpdomlem3  8441  unfi  8502  finsschain  8548  dffi3  8612  rankxplim3  9028  xpnum  9097  kmlem9  9302  sornom  9421  fpwwe2lem12  9785  cnegex  10543  zaddcl  11752  rexanre  14470  o1lo1  14652  o1co  14701  rlimcn2  14705  o1of2  14727  lo1add  14741  lo1mul  14742  summo  14832  ntrivcvgmul  15014  prodmolem2  15045  prodmo  15046  dvds2lem  15378  odd2np1  15446  opoe  15468  omoe  15469  opeo  15470  omeo  15471  bezoutlem4  15639  gcddiv  15648  divgcdcoprmex  15759  pcqmul  15936  pcadd  15971  mul4sq  16036  4sqlem12  16038  prmgaplem7  16139  gaorber  18098  psgneu  18284  lsmsubm  18426  pj1eu  18467  efgredlem  18519  efgredlemOLD  18520  efgrelexlemb  18523  qusabl  18628  cygabl  18652  dprdsubg  18784  dvdsrtr  19013  unitgrp  19028  lss1d  19329  lsmspsn  19450  lspsolvlem  19509  lbsextlem2  19527  znfld  20275  cygznlem3  20284  psgnghm  20292  tgcl  21151  restbas  21340  ordtbas2  21373  uncmp  21584  txuni2  21746  txbas  21748  ptbasin  21758  txcnp  21801  txlly  21817  txnlly  21818  tx1stc  21831  tx2ndc  21832  fbasrn  22065  rnelfmlem  22133  fmfnfmlem3  22137  txflf  22187  qustgplem  22301  trust  22410  utoptop  22415  fmucndlem  22472  blin2  22611  metustto  22735  tgqioo  22980  minveclem3b  23603  pmltpc  23623  evthicc2  23633  ovolunlem2  23671  dyaddisj  23769  rolle  24159  dvcvx  24189  itgsubst  24218  plyadd  24379  plymul  24380  coeeu  24387  aalioulem6  24498  dchrptlem2  25410  lgsdchr  25500  mul2sq  25564  2sqlem5  25567  pntibnd  25702  pntlemp  25719  cgraswap  26136  cgracom  26138  cgratr  26139  dfcgra2  26145  acopyeu  26150  ax5seg  26244  axpasch  26247  axeuclid  26269  axcontlem4  26273  axcontlem9  26278  uhgr2edg  26511  2pthon3v  27279  pjhthmo  28712  superpos  29764  chirredi  29804  cdjreui  29842  cdj3i  29851  xrofsup  30076  archiabllem2c  30290  ordtconnlem1  30511  dya2iocnrect  30884  txpconn  31756  cvmlift2lem10  31836  cvmlift3lem7  31849  msubco  31970  mclsppslem  32022  poseq  32287  soseq  32288  noprefixmo  32382  altopelaltxp  32617  funtransport  32672  btwnconn1lem13  32740  btwnconn1lem14  32741  segletr  32755  segleantisym  32756  funray  32781  funline  32783  tailfb  32905  mblfinlem3  33991  ismblfin  33993  itg2addnc  34006  ftc1anclem6  34032  heibor1lem  34149  crngohomfo  34346  ispridlc  34410  prter1  34953  hl2at  35479  cdlemn11pre  37284  dihord2pre  37299  dihord4  37332  dihmeetlem20N  37400  mapdpglem32  37779  diophin  38179  diophun  38180  iunrelexpuztr  38851  mullimc  40641  mullimcf  40648  addlimc  40673  fourierdlem42  41158  fourierdlem80  41195  sge0resplit  41412  hoiqssbllem3  41630  2reu4a  42012