Theorem rexlimivv 3178

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  r19.29vva  3196  2reu5  3716  2reu4  4477  opelxp  5660  elinxp  5978  reuop  6251  opiota  8003  f1o2ndf1  8064  poseq  8100  soseq  8101  tfrlem5  8311  xpdom2  9000  unxpdomlem3  9158  elfiun  9333  ttrcltr  9625  xpnum  9863  kmlem9  10069  nqereu  10840  distrlem5pr  10938  mulrid  11130  1re  11132  mul02  11311  cnegex  11314  recex  11769  creur  12139  creui  12140  cju  12141  elz2  12506  zaddcl  12531  qre  12866  qaddcl  12878  qnegcl  12879  qmulcl  12880  qreccl  12882  elpqb  12889  hash2prd  14398  elss2prb  14411  fundmge2nop0  14425  wrdl3s3  14885  replim  15039  prodmo  15859  odd2np1  16268  opoe  16290  omoe  16291  opeo  16292  omeo  16293  qredeu  16585  pythagtriplem1  16744  pcz  16809  4sqlem1  16876  4sqlem2  16877  4sqlem4  16880  mul4sq  16882  pmtr3ncom  19404  efgmnvl  19643  efgrelexlema  19678  ring1ne0  20234  pzriprnglem8  21443  txuni2  23509  tx2ndc  23595  blssioo  24739  tgioo  24740  ioorf  25530  ioorinv  25533  ioorcl  25534  dyaddisj  25553  mbfid  25592  elply  26156  vmacl  27084  efvmacl  27086  vmalelog  27172  2sqlem2  27385  mul2sq  27386  2sqlem7  27391  2sqnn0  27405  2sqreultblem  27415  pntibnd  27560  ostth  27606  cutsf  27788  zaddscl  28390  zmulscld  28393  elzn0s  28394  eln0zs  28396  zseo  28418  elz12s  28468  z12no  28472  z12addscl  28473  z12shalf  28476  z12zsodd  28478  z12bdaylem  28480  bdayfinlem  28482  remulscllem1  28496  legval  28656  upgredgpr  29215  nbgr2vtx1edg  29423  cusgredg  29497  usgredgsscusgredg  29533  wwlksnwwlksnon  29988  n4cyclfrgr  30366  vdgn1frgrv2  30371  friendshipgt3  30473  lpni  30555  nsnlplig  30556  nsnlpligALT  30557  n0lpligALT  30559  ipasslem5  30910  ipasslem11  30915  hhssnv  31339  shscli  31392  shsleji  31445  shsidmi  31459  spansncvi  31727  superpos  32429  chirredi  32469  mdsymlem6  32483  rnmposs  32752  1fldgenq  33404  ccfldextdgrr  33829  cnre2csqima  34068  dya2icobrsiga  34433  dya2iocnrect  34438  dya2iocucvr  34441  sxbrsigalem2  34443  afsval  34828  satfv0  35552  satfrnmapom  35564  satfv0fun  35565  satf00  35568  sat1el2xp  35573  fmla0xp  35577  fmla1  35581  msubco  35725  elaltxp  36169  altxpsspw  36171  funtransport  36225  funray  36334  funline  36336  ellines  36346  linethru  36347  icoreresf  37557  icoreclin  37562  relowlssretop  37568  relowlpssretop  37569  itg2addnc  37875  isline  39999  sn-it0e0  42671  sn-mullid  42691  sn-0tie0  42706  sn-mul02  42707  mzpcompact2lem  42993  sprvalpw  47726  sprvalpwn0  47729  prsprel  47733  prpair  47747  prprvalpw  47761  reuopreuprim  47772  nnsum3primesgbe  48038  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  tgblthelfgott  48061  grtrif1o  48188  grtrissvtx  48190  gpgvtxel2  48294  pgn4cyclex  48372  nnpw2pb  48833  2arymaptf1  48899