Theorem rexlimivv 3180

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)

Hypothesis

Ref	Expression
rexlimivv.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓))

Assertion

Ref	Expression
rexlimivv	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓)

Distinct variable groups:   𝑥,𝑦,𝜓   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimivv

Step	Hyp	Ref	Expression
1		rexlimivv.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝜓))
2	1	rexlimdva 3139	. 2 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → 𝜓))
3	2	rexlimiv 3132	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ 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-rex 3063

This theorem is referenced by:  r19.29vva  3198  2reu5  3718  2reu4  4479  opelxp  5668  elinxp  5986  reuop  6259  opiota  8013  f1o2ndf1  8074  poseq  8110  soseq  8111  tfrlem5  8321  xpdom2  9012  unxpdomlem3  9170  elfiun  9345  ttrcltr  9637  xpnum  9875  kmlem9  10081  nqereu  10852  distrlem5pr  10950  mulrid  11142  1re  11144  mul02  11323  cnegex  11326  recex  11781  creur  12151  creui  12152  cju  12153  elz2  12518  zaddcl  12543  qre  12878  qaddcl  12890  qnegcl  12891  qmulcl  12892  qreccl  12894  elpqb  12901  hash2prd  14410  elss2prb  14423  fundmge2nop0  14437  wrdl3s3  14897  replim  15051  prodmo  15871  odd2np1  16280  opoe  16302  omoe  16303  opeo  16304  omeo  16305  qredeu  16597  pythagtriplem1  16756  pcz  16821  4sqlem1  16888  4sqlem2  16889  4sqlem4  16892  mul4sq  16894  pmtr3ncom  19416  efgmnvl  19655  efgrelexlema  19690  ring1ne0  20246  pzriprnglem8  21455  txuni2  23521  tx2ndc  23607  blssioo  24751  tgioo  24752  ioorf  25542  ioorinv  25545  ioorcl  25546  dyaddisj  25565  mbfid  25604  elply  26168  vmacl  27096  efvmacl  27098  vmalelog  27184  2sqlem2  27397  mul2sq  27398  2sqlem7  27403  2sqnn0  27417  2sqreultblem  27427  pntibnd  27572  ostth  27618  cutsf  27800  zaddscl  28402  zmulscld  28405  elzn0s  28406  eln0zs  28408  zseo  28430  elz12s  28480  z12no  28484  z12addscl  28485  z12shalf  28488  z12zsodd  28490  z12bdaylem  28492  bdayfinlem  28494  remulscllem1  28508  legval  28668  upgredgpr  29227  nbgr2vtx1edg  29435  cusgredg  29509  usgredgsscusgredg  29545  wwlksnwwlksnon  30000  n4cyclfrgr  30378  vdgn1frgrv2  30383  friendshipgt3  30485  lpni  30568  nsnlplig  30569  nsnlpligALT  30570  n0lpligALT  30572  ipasslem5  30923  ipasslem11  30928  hhssnv  31352  shscli  31405  shsleji  31458  shsidmi  31472  spansncvi  31740  superpos  32442  chirredi  32482  mdsymlem6  32496  rnmposs  32763  1fldgenq  33416  ccfldextdgrr  33850  cnre2csqima  34089  dya2icobrsiga  34454  dya2iocnrect  34459  dya2iocucvr  34462  sxbrsigalem2  34464  afsval  34849  satfv0  35574  satfrnmapom  35586  satfv0fun  35587  satf00  35590  sat1el2xp  35595  fmla0xp  35599  fmla1  35603  msubco  35747  elaltxp  36191  altxpsspw  36193  funtransport  36247  funray  36356  funline  36358  ellines  36368  linethru  36369  icoreresf  37607  icoreclin  37612  relowlssretop  37618  relowlpssretop  37619  itg2addnc  37925  isline  40115  sn-it0e0  42786  sn-mullid  42806  sn-0tie0  42821  sn-mul02  42822  mzpcompact2lem  43108  sprvalpw  47840  sprvalpwn0  47843  prsprel  47847  prpair  47861  prprvalpw  47875  reuopreuprim  47886  nnsum3primesgbe  48152  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  tgblthelfgott  48175  grtrif1o  48302  grtrissvtx  48304  gpgvtxel2  48408  pgn4cyclex  48486  nnpw2pb  48947  2arymaptf1  49013