Theorem reeanv 3207

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		exdistrv 1955	. 2 ⊢ (∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐵 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜓)))
2	1	reeanlem 3206	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  3reeanv  3208  2reu4lem  4481  disjxiun  5099  fliftfun  7269  poseq  8114  soseq  8115  frrlem9  8250  tfrlem5  8325  uniinqs  8747  eroveu  8762  erovlem  8763  xpf1o  9080  unxpdomlem3  9175  finsschain  9286  dffi3  9358  ttrcltr  9645  rankxplim3  9810  xpnum  9880  kmlem9  10088  sornom  10206  fpwwe2lem11  10570  cnegex  11331  zaddcl  12549  rexanre  15289  o1lo1  15479  o1co  15528  rlimcn3  15532  o1of2  15555  lo1add  15569  lo1mul  15570  summo  15659  ntrivcvgmul  15844  prodmolem2  15877  prodmo  15878  dvds2lem  16214  odd2np1  16287  opoe  16309  omoe  16310  opeo  16311  omeo  16312  bezoutlem4  16488  gcddiv  16497  divgcdcoprmex  16612  pcqmul  16800  pcadd  16836  mul4sq  16901  4sqlem12  16903  prmgaplem7  17004  cyccom  19117  gaorber  19222  psgneu  19420  lsmsubm  19567  pj1eu  19610  efgredlem  19661  efgrelexlemb  19664  qusabl  19779  dprdsubg  19940  dvdsrtr  20288  unitgrp  20303  lss1d  20901  lsmspsn  21023  lspsolvlem  21084  lbsextlem2  21101  znfld  21502  cygznlem3  21511  psgnghm  21522  tgcl  22889  restbas  23078  ordtbas2  23111  uncmp  23323  txuni2  23485  txbas  23487  ptbasin  23497  txcnp  23540  txlly  23556  txnlly  23557  tx1stc  23570  tx2ndc  23571  fbasrn  23804  rnelfmlem  23872  fmfnfmlem3  23876  txflf  23926  qustgplem  24041  trust  24150  utoptop  24155  fmucndlem  24211  blin2  24350  metustto  24474  tgqioo  24721  minveclem3b  25361  pmltpc  25384  evthicc2  25394  ovolunlem2  25432  dyaddisj  25530  rolle  25927  dvcvx  25958  itgsubst  25989  plyadd  26155  plymul  26156  coeeu  26163  aalioulem6  26278  dchrptlem2  27209  lgsdchr  27299  mul2sq  27363  2sqlem5  27366  pntibnd  27537  pntlemp  27554  nosupprefixmo  27645  noinfprefixmo  27646  addsproplem2  27917  negsproplem2  27975  mulsuniflem  28092  precsexlem10  28158  zaddscl  28322  zmulscld  28325  zseo  28349  zs12addscl  28389  recut  28400  readdscl  28403  remulscl  28406  cgraswap  28800  cgracom  28802  cgratr  28803  flatcgra  28804  dfcgra2  28810  acopyeu  28814  ax5seg  28918  axpasch  28921  axeuclid  28943  axcontlem4  28947  axcontlem9  28952  uhgr2edg  29188  2pthon3v  29923  pjhthmo  31281  superpos  32333  chirredi  32373  cdjreui  32411  cdj3i  32420  xrofsup  32740  archiabllem2c  33164  ccfldextdgrr  33660  ordtconnlem1  33907  dya2iocnrect  34265  txpconn  35212  cvmlift2lem10  35292  cvmlift3lem7  35305  msubco  35511  mclsppslem  35563  altopelaltxp  35957  funtransport  36012  btwnconn1lem13  36080  btwnconn1lem14  36081  segletr  36095  segleantisym  36096  funray  36121  funline  36123  tailfb  36358  mblfinlem3  37646  ismblfin  37648  itg2addnc  37661  ftc1anclem6  37685  heibor1lem  37796  crngohomfo  37993  ispridlc  38057  prter1  38865  hl2at  39392  cdlemn11pre  41197  dihord2pre  41212  dihord4  41245  dihmeetlem20N  41313  mapdpglem32  41692  diophin  42753  diophun  42754  iunrelexpuztr  43701  mullimc  45607  mullimcf  45614  addlimc  45639  fourierdlem42  46140  fourierdlem80  46177  sge0resplit  46397  hoiqssbllem3  46615