Theorem reeanv 3226

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-ral 3059  df-rex 3068

This theorem is referenced by:  3reeanv  3227  2ralorOLD  3229  2reu4lem  4527  disjxiun  5144  fliftfun  7331  poseq  8181  soseq  8182  frrlem9  8317  tfrlem5  8418  uniinqs  8835  eroveu  8850  erovlem  8851  xpf1o  9177  unxpdomlem3  9285  finsschain  9396  dffi3  9468  ttrcltr  9753  rankxplim3  9918  xpnum  9988  kmlem9  10196  sornom  10314  fpwwe2lem11  10678  cnegex  11439  zaddcl  12654  rexanre  15381  o1lo1  15569  o1co  15618  rlimcn3  15622  o1of2  15645  lo1add  15659  lo1mul  15660  summo  15749  ntrivcvgmul  15934  prodmolem2  15967  prodmo  15968  dvds2lem  16302  odd2np1  16374  opoe  16396  omoe  16397  opeo  16398  omeo  16399  bezoutlem4  16575  gcddiv  16584  divgcdcoprmex  16699  pcqmul  16886  pcadd  16922  mul4sq  16987  4sqlem12  16989  prmgaplem7  17090  cyccom  19233  gaorber  19338  psgneu  19538  lsmsubm  19685  pj1eu  19728  efgredlem  19779  efgrelexlemb  19782  qusabl  19897  dprdsubg  20058  dvdsrtr  20384  unitgrp  20399  lss1d  20978  lsmspsn  21100  lspsolvlem  21161  lbsextlem2  21178  znfld  21596  cygznlem3  21605  psgnghm  21615  tgcl  22991  restbas  23181  ordtbas2  23214  uncmp  23426  txuni2  23588  txbas  23590  ptbasin  23600  txcnp  23643  txlly  23659  txnlly  23660  tx1stc  23673  tx2ndc  23674  fbasrn  23907  rnelfmlem  23975  fmfnfmlem3  23979  txflf  24029  qustgplem  24144  trust  24253  utoptop  24258  fmucndlem  24315  blin2  24454  metustto  24581  tgqioo  24835  minveclem3b  25475  pmltpc  25498  evthicc2  25508  ovolunlem2  25546  dyaddisj  25644  rolle  26042  dvcvx  26073  itgsubst  26104  plyadd  26270  plymul  26271  coeeu  26278  aalioulem6  26393  dchrptlem2  27323  lgsdchr  27413  mul2sq  27477  2sqlem5  27480  pntibnd  27651  pntlemp  27668  nosupprefixmo  27759  noinfprefixmo  27760  addsproplem2  28017  negsproplem2  28075  mulsuniflem  28189  precsexlem10  28254  zaddscl  28394  zmulscld  28397  zseo  28420  recut  28442  readdscl  28445  remulscl  28448  cgraswap  28842  cgracom  28844  cgratr  28845  flatcgra  28846  dfcgra2  28852  acopyeu  28856  ax5seg  28967  axpasch  28970  axeuclid  28992  axcontlem4  28996  axcontlem9  29001  uhgr2edg  29239  2pthon3v  29972  pjhthmo  31330  superpos  32382  chirredi  32422  cdjreui  32460  cdj3i  32469  xrofsup  32777  archiabllem2c  33184  ccfldextdgrr  33696  ordtconnlem1  33884  dya2iocnrect  34262  txpconn  35216  cvmlift2lem10  35296  cvmlift3lem7  35309  msubco  35515  mclsppslem  35567  altopelaltxp  35957  funtransport  36012  btwnconn1lem13  36080  btwnconn1lem14  36081  segletr  36095  segleantisym  36096  funray  36121  funline  36123  tailfb  36359  mblfinlem3  37645  ismblfin  37647  itg2addnc  37660  ftc1anclem6  37684  heibor1lem  37795  crngohomfo  37992  ispridlc  38056  prter1  38860  hl2at  39387  cdlemn11pre  41192  dihord2pre  41207  dihord4  41240  dihmeetlem20N  41308  mapdpglem32  41687  diophin  42759  diophun  42760  iunrelexpuztr  43708  mullimc  45571  mullimcf  45578  addlimc  45603  fourierdlem42  46104  fourierdlem80  46141  sge0resplit  46361  hoiqssbllem3  46579