Theorem reeanv 3209

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 3208	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  3210  2reu4lem  4485  disjxiun  5104  fliftfun  7287  poseq  8137  soseq  8138  frrlem9  8273  tfrlem5  8348  uniinqs  8770  eroveu  8785  erovlem  8786  xpf1o  9103  unxpdomlem3  9199  finsschain  9310  dffi3  9382  ttrcltr  9669  rankxplim3  9834  xpnum  9904  kmlem9  10112  sornom  10230  fpwwe2lem11  10594  cnegex  11355  zaddcl  12573  rexanre  15313  o1lo1  15503  o1co  15552  rlimcn3  15556  o1of2  15579  lo1add  15593  lo1mul  15594  summo  15683  ntrivcvgmul  15868  prodmolem2  15901  prodmo  15902  dvds2lem  16238  odd2np1  16311  opoe  16333  omoe  16334  opeo  16335  omeo  16336  bezoutlem4  16512  gcddiv  16521  divgcdcoprmex  16636  pcqmul  16824  pcadd  16860  mul4sq  16925  4sqlem12  16927  prmgaplem7  17028  cyccom  19135  gaorber  19240  psgneu  19436  lsmsubm  19583  pj1eu  19626  efgredlem  19677  efgrelexlemb  19680  qusabl  19795  dprdsubg  19956  dvdsrtr  20277  unitgrp  20292  lss1d  20869  lsmspsn  20991  lspsolvlem  21052  lbsextlem2  21069  znfld  21470  cygznlem3  21479  psgnghm  21489  tgcl  22856  restbas  23045  ordtbas2  23078  uncmp  23290  txuni2  23452  txbas  23454  ptbasin  23464  txcnp  23507  txlly  23523  txnlly  23524  tx1stc  23537  tx2ndc  23538  fbasrn  23771  rnelfmlem  23839  fmfnfmlem3  23843  txflf  23893  qustgplem  24008  trust  24117  utoptop  24122  fmucndlem  24178  blin2  24317  metustto  24441  tgqioo  24688  minveclem3b  25328  pmltpc  25351  evthicc2  25361  ovolunlem2  25399  dyaddisj  25497  rolle  25894  dvcvx  25925  itgsubst  25956  plyadd  26122  plymul  26123  coeeu  26130  aalioulem6  26245  dchrptlem2  27176  lgsdchr  27266  mul2sq  27330  2sqlem5  27333  pntibnd  27504  pntlemp  27521  nosupprefixmo  27612  noinfprefixmo  27613  addsproplem2  27877  negsproplem2  27935  mulsuniflem  28052  precsexlem10  28118  zaddscl  28282  zmulscld  28285  zseo  28308  recut  28347  readdscl  28350  remulscl  28353  cgraswap  28747  cgracom  28749  cgratr  28750  flatcgra  28751  dfcgra2  28757  acopyeu  28761  ax5seg  28865  axpasch  28868  axeuclid  28890  axcontlem4  28894  axcontlem9  28899  uhgr2edg  29135  2pthon3v  29873  pjhthmo  31231  superpos  32283  chirredi  32323  cdjreui  32361  cdj3i  32370  xrofsup  32690  archiabllem2c  33149  ccfldextdgrr  33667  ordtconnlem1  33914  dya2iocnrect  34272  txpconn  35219  cvmlift2lem10  35299  cvmlift3lem7  35312  msubco  35518  mclsppslem  35570  altopelaltxp  35964  funtransport  36019  btwnconn1lem13  36087  btwnconn1lem14  36088  segletr  36102  segleantisym  36103  funray  36128  funline  36130  tailfb  36365  mblfinlem3  37653  ismblfin  37655  itg2addnc  37668  ftc1anclem6  37692  heibor1lem  37803  crngohomfo  38000  ispridlc  38064  prter1  38872  hl2at  39399  cdlemn11pre  41204  dihord2pre  41219  dihord4  41252  dihmeetlem20N  41320  mapdpglem32  41699  diophin  42760  diophun  42761  iunrelexpuztr  43708  mullimc  45614  mullimcf  45621  addlimc  45646  fourierdlem42  46147  fourierdlem80  46184  sge0resplit  46404  hoiqssbllem3  46622