Theorem reeanv 3238

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2146  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3081  df-rex 3091

This theorem is used by:  3reeanv  3239  2reu4lem  4482  disjxiun  5103  fliftfun  7330  poseq  8188  soseq  8189  frrlem9  8326  tfrlem5  8401  uniinqs  8832  eroveu  8847  erovlem  8848  xpf1o  9172  unxpdomlem3  9263  finsschain  9362  dffi3  9436  ttrcltr  9730  rankxplim3  9911  xpnum  10045  kmlem9  10250  sornom  10368  fpwwe2lem11  10739  cnegex  11504  zaddcl  12749  rexanre  15529  o1lo1  15719  o1co  15768  rlimcn3  15772  o1of2  15795  lo1add  15809  lo1mul  15810  summo  15898  ntrivcvgmul  16086  prodmolem2  16117  prodmo  16118  dvds2lem  16453  odd2np1  16526  opoe  16548  omoe  16549  opeo  16550  omeo  16551  bezoutlem4  16730  gcddiv  16739  divgcdcoprmex  16856  pcqmul  17046  pcadd  17082  mul4sq  17147  4sqlem12  17149  prmgaplem7  17250  cyccom  19433  gaorber  19537  psgneu  19735  lsmsubm  19882  pj1eu  19925  efgredlem  19976  efgrelexlemb  19979  qusabl  20094  dprdsubg  20255  dvdsrtr  20613  unitgrp  20628  crngrhmfo  20741  lss1d  21253  lsmspsn  21374  lspsolvlem  21435  lbsextlem2  21452  znfld  21881  cygznlem3  21890  psgnghm  21901  tgcl  23302  restbas  23491  ordtbas2  23524  uncmp  23736  txuni2  23899  txbas  23901  ptbasin  23911  txcnp  23954  txlly  23970  txnlly  23971  tx1stc  23984  tx2ndc  23985  fbasrn  24218  rnelfmlem  24286  fmfnfmlem3  24290  txflf  24340  qustgplem  24455  trust  24563  utoptop  24568  fmucndlem  24624  blin2  24763  metustto  24887  tgqioo  25134  minveclem3b  25764  pmltpc  25786  evthicc2  25796  ovolunlem2  25834  dyaddisj  25932  rolle  26325  dvcvx  26355  itgsubst  26384  plyadd  26551  plymul  26552  coeeu  26559  aalioulem6  26679  dchrptlem2  27607  lgsdchr  27697  mul2sq  27761  2sqlem5  27764  pntibnd  27935  pntlemp  27952  nosupprefixmo  28072  noinfprefixmo  28073  addsproplem2  28371  negsproplem2  28430  mulsuniflem  28550  precsexlem10  28617  zaddscl  28795  zmulscld  28798  zseo  28823  z12addscl  28878  recut  28895  readdscl  28900  remulscl  28903  cgraswap  29342  cgracom  29344  cgratr  29345  flatcgra  29347  dfcgra2  29353  acopyeu  29357  ax5seg  29531  axpasch  29534  axeuclid  29556  axcontlem4  29560  axcontlem9  29565  uhgr2edg  29804  2pthon3v  30547  pjhthmo  31919  superpos  32971  chirredi  33011  cdjreui  33049  cdj3i  33058  cgrahlb  33062  xrofsup  33415  archiabllem2c  33812  ccfldextdgrr  34360  ordtconnlem1  34612  dya2iocnrect  34969  txpconn  36121  cvmlift2lem10  36201  cvmlift3lem7  36214  msubco  36420  mclsppslem  36472  altopelaltxp  36874  funtransport  36929  btwnconn1lem13  36997  btwnconn1lem14  36998  segletr  37012  segleantisym  37013  funray  37038  funline  37040  tailfb  37298  mblfinlem3  38723  ismblfin  38725  itg2addnc  38738  ftc1anclem6  38762  heibor1lem  38889  crngohomfo  39086  ispridlc  39150  prter1  40082  hl2at  40608  cdlemn11pre  42413  dihord2pre  42428  dihord4  42461  dihmeetlem20N  42529  mapdpglem32  42908  diophin  43929  diophun  43930  iunrelexpuztr  44865  mullimc  46773  mullimcf  46780  addlimc  46803  fourierdlem42  47304  fourierdlem80  47341  sge0resplit  47561  hoiqssbllem3  47779