Theorem reeanv 3086

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 1830	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1830	. 2 ⊢ Ⅎ𝑥𝜓
3	1, 2	reean 3085	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-ral 2901  df-rex 2902

This theorem is referenced by:  3reeanv  3087  2ralor  3088  disjxiun  4579  disjxiunOLD  4580  fliftfun  6462  tfrlem5  7363  uniinqs  7714  eroveu  7729  erovlem  7730  xpf1o  8007  unxpdomlem3  8051  unfi  8112  finsschain  8156  dffi3  8220  rankxplim3  8627  xpnum  8660  kmlem9  8863  sornom  8982  fpwwe2lem12  9342  cnegex  10096  zaddcl  11294  rexanre  13934  o1lo1  14116  o1co  14165  rlimcn2  14169  o1of2  14191  lo1add  14205  lo1mul  14206  summo  14295  ntrivcvgmul  14473  prodmolem2  14504  prodmo  14505  dvds2lem  14832  odd2np1  14903  opoe  14925  omoe  14926  opeo  14927  omeo  14928  bezoutlem4  15097  gcddiv  15106  divgcdcoprmex  15218  pcqmul  15396  pcadd  15431  mul4sq  15496  4sqlem12  15498  prmgaplem7  15599  gaorber  17564  psgneu  17749  lsmsubm  17891  pj1eu  17932  efgredlem  17983  efgrelexlemb  17986  qusabl  18091  cygabl  18115  dprdsubg  18246  dvdsrtr  18475  unitgrp  18490  lss1d  18784  lsmspsn  18905  lspsolvlem  18963  lbsextlem2  18980  znfld  19728  cygznlem3  19737  psgnghm  19745  tgcl  20584  restbas  20772  ordtbas2  20805  uncmp  21016  txuni2  21178  txbas  21180  ptbasin  21190  txcnp  21233  txlly  21249  txnlly  21250  tx1stc  21263  tx2ndc  21264  fbasrn  21498  rnelfmlem  21566  fmfnfmlem3  21570  txflf  21620  qustgplem  21734  trust  21843  utoptop  21848  fmucndlem  21905  blin2  22044  metustto  22168  tgqioo  22411  minveclem3b  23007  pmltpc  23026  evthicc2  23036  ovolunlem2  23073  dyaddisj  23170  rolle  23557  dvcvx  23587  itgsubst  23616  plyadd  23777  plymul  23778  coeeu  23785  aalioulem6  23896  dchrptlem2  24790  lgsdchr  24880  mul2sq  24944  2sqlem5  24947  pntibnd  25082  pntlemp  25099  cgraswap  25512  cgracom  25514  cgratr  25515  dfcgra2  25521  acopyeu  25525  ax5seg  25618  axpasch  25621  axeuclid  25643  axcontlem4  25647  axcontlem9  25652  usgra2edg  25911  frgrawopreglem5  26575  pjhthmo  27545  superpos  28597  chirredi  28637  cdjreui  28675  cdj3i  28684  xrofsup  28923  archiabllem2c  29080  ordtconlem1  29298  dya2iocnrect  29670  txpcon  30468  cvmlift2lem10  30548  cvmlift3lem7  30561  msubco  30682  mclsppslem  30734  poseq  30994  soseq  30995  altopelaltxp  31253  funtransport  31308  btwnconn1lem13  31376  btwnconn1lem14  31377  segletr  31391  segleantisym  31392  funray  31417  funline  31419  tailfb  31542  mblfinlem3  32618  ismblfin  32620  itg2addnc  32634  ftc1anclem6  32660  heibor1lem  32778  crngohomfo  32975  ispridlc  33039  prter1  33182  hl2at  33709  cdlemn11pre  35517  dihord2pre  35532  dihord4  35565  dihmeetlem20N  35633  mapdpglem32  36012  diophin  36354  diophun  36355  iunrelexpuztr  37030  mullimc  38683  mullimcf  38690  addlimc  38715  fourierdlem42  39042  fourierdlem80  39079  sge0resplit  39299  hoiqssbllem3  39514  2reu4a  39838  uhgr2edg  40435  2pthon3v-av  41150  frgrwopreglem5  41485