Theorem reeanv 3107

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		nfv 1843	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1843	. 2 ⊢ Ⅎ𝑥𝜓
3	1, 2	reean 3106	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 384  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-ral 2917  df-rex 2918

This theorem is referenced by:  3reeanv  3108  2ralor  3109  disjxiun  4649  disjxiunOLD  4650  fliftfun  6562  tfrlem5  7476  uniinqs  7827  eroveu  7842  erovlem  7843  xpf1o  8122  unxpdomlem3  8166  unfi  8227  finsschain  8273  dffi3  8337  rankxplim3  8744  xpnum  8777  kmlem9  8980  sornom  9099  fpwwe2lem12  9463  cnegex  10217  zaddcl  11417  rexanre  14086  o1lo1  14268  o1co  14317  rlimcn2  14321  o1of2  14343  lo1add  14357  lo1mul  14358  summo  14448  ntrivcvgmul  14634  prodmolem2  14665  prodmo  14666  dvds2lem  14994  odd2np1  15065  opoe  15087  omoe  15088  opeo  15089  omeo  15090  bezoutlem4  15259  gcddiv  15268  divgcdcoprmex  15380  pcqmul  15558  pcadd  15593  mul4sq  15658  4sqlem12  15660  prmgaplem7  15761  gaorber  17741  psgneu  17926  lsmsubm  18068  pj1eu  18109  efgredlem  18160  efgrelexlemb  18163  qusabl  18268  cygabl  18292  dprdsubg  18423  dvdsrtr  18652  unitgrp  18667  lss1d  18963  lsmspsn  19084  lspsolvlem  19142  lbsextlem2  19159  znfld  19909  cygznlem3  19918  psgnghm  19926  tgcl  20773  restbas  20962  ordtbas2  20995  uncmp  21206  txuni2  21368  txbas  21370  ptbasin  21380  txcnp  21423  txlly  21439  txnlly  21440  tx1stc  21453  tx2ndc  21454  fbasrn  21688  rnelfmlem  21756  fmfnfmlem3  21760  txflf  21810  qustgplem  21924  trust  22033  utoptop  22038  fmucndlem  22095  blin2  22234  metustto  22358  tgqioo  22603  minveclem3b  23199  pmltpc  23219  evthicc2  23229  ovolunlem2  23266  dyaddisj  23364  rolle  23753  dvcvx  23783  itgsubst  23812  plyadd  23973  plymul  23974  coeeu  23981  aalioulem6  24092  dchrptlem2  24990  lgsdchr  25080  mul2sq  25144  2sqlem5  25147  pntibnd  25282  pntlemp  25299  cgraswap  25712  cgracom  25714  cgratr  25715  dfcgra2  25721  acopyeu  25725  ax5seg  25818  axpasch  25821  axeuclid  25843  axcontlem4  25847  axcontlem9  25852  uhgr2edg  26100  2pthon3v  26839  pjhthmo  28161  superpos  29213  chirredi  29253  cdjreui  29291  cdj3i  29300  xrofsup  29533  archiabllem2c  29749  ordtconnlem1  29970  dya2iocnrect  30343  txpconn  31214  cvmlift2lem10  31294  cvmlift3lem7  31307  msubco  31428  mclsppslem  31480  poseq  31750  soseq  31751  noprefixmo  31848  altopelaltxp  32083  funtransport  32138  btwnconn1lem13  32206  btwnconn1lem14  32207  segletr  32221  segleantisym  32222  funray  32247  funline  32249  tailfb  32372  mblfinlem3  33448  ismblfin  33450  itg2addnc  33464  ftc1anclem6  33490  heibor1lem  33608  crngohomfo  33805  ispridlc  33869  prter1  34164  hl2at  34691  cdlemn11pre  36499  dihord2pre  36514  dihord4  36547  dihmeetlem20N  36615  mapdpglem32  36994  diophin  37336  diophun  37337  iunrelexpuztr  38011  mullimc  39848  mullimcf  39855  addlimc  39880  fourierdlem42  40366  fourierdlem80  40403  sge0resplit  40623  hoiqssbllem3  40838  2reu4a  41189