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 3135	. 2 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → 𝜓))
3	2	rexlimiv 3128	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3054

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-rex 3055

This theorem is referenced by:  r19.29vva  3198  2reu5  3732  2reu4  4489  opelxp  5677  elinxp  5993  reuop  6269  opiota  8041  f1o2ndf1  8104  poseq  8140  soseq  8141  tfrlem5  8351  xpdom2  9041  1sdomOLD  9203  unxpdomlem3  9206  elfiun  9388  ttrcltr  9676  xpnum  9911  kmlem9  10119  nqereu  10889  distrlem5pr  10987  mulrid  11179  1re  11181  mul02  11359  cnegex  11362  recex  11817  creur  12187  creui  12188  cju  12189  elz2  12554  zaddcl  12580  qre  12919  qaddcl  12931  qnegcl  12932  qmulcl  12933  qreccl  12935  elpqb  12942  hash2prd  14447  elss2prb  14460  fundmge2nop0  14474  wrdl3s3  14935  replim  15089  prodmo  15909  odd2np1  16318  opoe  16340  omoe  16341  opeo  16342  omeo  16343  qredeu  16635  pythagtriplem1  16794  pcz  16859  4sqlem1  16926  4sqlem2  16927  4sqlem4  16930  mul4sq  16932  pmtr3ncom  19412  efgmnvl  19651  efgrelexlema  19686  ring1ne0  20215  pzriprnglem8  21405  txuni2  23459  tx2ndc  23545  blssioo  24690  tgioo  24691  ioorf  25481  ioorinv  25484  ioorcl  25485  dyaddisj  25504  mbfid  25543  elply  26107  vmacl  27035  efvmacl  27037  vmalelog  27123  2sqlem2  27336  mul2sq  27337  2sqlem7  27342  2sqnn0  27356  2sqreultblem  27366  pntibnd  27511  ostth  27557  scutf  27731  zaddscl  28289  zmulscld  28292  elzn0s  28293  eln0zs  28295  zseo  28315  elzs12  28344  zs12bday  28350  remulscllem1  28358  legval  28518  upgredgpr  29076  nbgr2vtx1edg  29284  cusgredg  29358  usgredgsscusgredg  29394  wwlksnwwlksnon  29852  n4cyclfrgr  30227  vdgn1frgrv2  30232  friendshipgt3  30334  lpni  30416  nsnlplig  30417  nsnlpligALT  30418  n0lpligALT  30420  ipasslem5  30771  ipasslem11  30776  hhssnv  31200  shscli  31253  shsleji  31306  shsidmi  31320  spansncvi  31588  superpos  32290  chirredi  32330  mdsymlem6  32344  rnmposs  32605  1fldgenq  33279  ccfldextdgrr  33674  cnre2csqima  33908  dya2icobrsiga  34274  dya2iocnrect  34279  dya2iocucvr  34282  sxbrsigalem2  34284  afsval  34669  satfv0  35352  satfrnmapom  35364  satfv0fun  35365  satf00  35368  sat1el2xp  35373  fmla0xp  35377  fmla1  35381  msubco  35525  elaltxp  35970  altxpsspw  35972  funtransport  36026  funray  36135  funline  36137  ellines  36147  linethru  36148  icoreresf  37347  icoreclin  37352  relowlssretop  37358  relowlpssretop  37359  itg2addnc  37675  isline  39740  sn-it0e0  42411  sn-mullid  42431  sn-0tie0  42446  sn-mul02  42447  mzpcompact2lem  42746  sprvalpw  47485  sprvalpwn0  47488  prsprel  47492  prpair  47506  prprvalpw  47520  reuopreuprim  47531  nnsum3primesgbe  47797  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  tgblthelfgott  47820  grtrif1o  47945  grtrissvtx  47947  gpgvtxel2  48043  pgn4cyclex  48120  nnpw2pb  48580  2arymaptf1  48646