Theorem reeanv 3210

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053  df-rex 3063

This theorem is referenced by:  3reeanv  3211  2reu4lem  4478  disjxiun  5097  fliftfun  7268  poseq  8110  soseq  8111  frrlem9  8246  tfrlem5  8321  uniinqs  8746  eroveu  8761  erovlem  8762  xpf1o  9079  unxpdomlem3  9170  finsschain  9271  dffi3  9346  ttrcltr  9637  rankxplim3  9805  xpnum  9875  kmlem9  10081  sornom  10199  fpwwe2lem11  10564  cnegex  11326  zaddcl  12543  rexanre  15282  o1lo1  15472  o1co  15521  rlimcn3  15525  o1of2  15548  lo1add  15562  lo1mul  15563  summo  15652  ntrivcvgmul  15837  prodmolem2  15870  prodmo  15871  dvds2lem  16207  odd2np1  16280  opoe  16302  omoe  16303  opeo  16304  omeo  16305  bezoutlem4  16481  gcddiv  16490  divgcdcoprmex  16605  pcqmul  16793  pcadd  16829  mul4sq  16894  4sqlem12  16896  prmgaplem7  16997  cyccom  19147  gaorber  19252  psgneu  19450  lsmsubm  19597  pj1eu  19640  efgredlem  19691  efgrelexlemb  19694  qusabl  19809  dprdsubg  19970  dvdsrtr  20319  unitgrp  20334  lss1d  20929  lsmspsn  21051  lspsolvlem  21112  lbsextlem2  21129  znfld  21530  cygznlem3  21539  psgnghm  21550  tgcl  22928  restbas  23117  ordtbas2  23150  uncmp  23362  txuni2  23524  txbas  23526  ptbasin  23536  txcnp  23579  txlly  23595  txnlly  23596  tx1stc  23609  tx2ndc  23610  fbasrn  23843  rnelfmlem  23911  fmfnfmlem3  23915  txflf  23965  qustgplem  24080  trust  24188  utoptop  24193  fmucndlem  24249  blin2  24388  metustto  24512  tgqioo  24759  minveclem3b  25399  pmltpc  25422  evthicc2  25432  ovolunlem2  25470  dyaddisj  25568  rolle  25965  dvcvx  25996  itgsubst  26027  plyadd  26193  plymul  26194  coeeu  26201  aalioulem6  26316  dchrptlem2  27247  lgsdchr  27337  mul2sq  27401  2sqlem5  27404  pntibnd  27575  pntlemp  27592  nosupprefixmo  27683  noinfprefixmo  27684  addsproplem2  27981  negsproplem2  28040  mulsuniflem  28160  precsexlem10  28227  zaddscl  28405  zmulscld  28408  zseo  28433  z12addscl  28488  recut  28505  readdscl  28510  remulscl  28513  cgraswap  28908  cgracom  28910  cgratr  28911  flatcgra  28912  dfcgra2  28918  acopyeu  28922  ax5seg  29027  axpasch  29030  axeuclid  29052  axcontlem4  29056  axcontlem9  29061  uhgr2edg  29297  2pthon3v  30032  pjhthmo  31394  superpos  32446  chirredi  32486  cdjreui  32524  cdj3i  32533  xrofsup  32862  archiabllem2c  33293  ccfldextdgrr  33854  ordtconnlem1  34106  dya2iocnrect  34463  txpconn  35452  cvmlift2lem10  35532  cvmlift3lem7  35545  msubco  35751  mclsppslem  35803  altopelaltxp  36196  funtransport  36251  btwnconn1lem13  36319  btwnconn1lem14  36320  segletr  36334  segleantisym  36335  funray  36360  funline  36362  tailfb  36597  mblfinlem3  37914  ismblfin  37916  itg2addnc  37929  ftc1anclem6  37953  heibor1lem  38064  crngohomfo  38261  ispridlc  38325  prter1  39259  hl2at  39785  cdlemn11pre  41590  dihord2pre  41605  dihord4  41638  dihmeetlem20N  41706  mapdpglem32  42085  diophin  43133  diophun  43134  iunrelexpuztr  44079  mullimc  45980  mullimcf  45987  addlimc  46010  fourierdlem42  46511  fourierdlem80  46548  sge0resplit  46768  hoiqssbllem3  46986