Theorem rexlimivv 3179

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3061

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 3062

This theorem is referenced by:  r19.29vva  3197  2reu5  3704  2reu4  4464  opelxp  5667  elinxp  5984  reuop  6257  opiota  8012  f1o2ndf1  8072  poseq  8108  soseq  8109  tfrlem5  8319  xpdom2  9010  unxpdomlem3  9168  elfiun  9343  ttrcltr  9637  xpnum  9875  kmlem9  10081  nqereu  10852  distrlem5pr  10950  mulrid  11142  1re  11144  mul02  11324  cnegex  11327  recex  11782  creur  12153  creui  12154  cju  12155  elz2  12542  zaddcl  12567  qre  12903  qaddcl  12915  qnegcl  12916  qmulcl  12917  qreccl  12919  elpqb  12926  hash2prd  14437  elss2prb  14450  fundmge2nop0  14464  wrdl3s3  14924  replim  15078  prodmo  15901  odd2np1  16310  opoe  16332  omoe  16333  opeo  16334  omeo  16335  qredeu  16627  pythagtriplem1  16787  pcz  16852  4sqlem1  16919  4sqlem2  16920  4sqlem4  16923  mul4sq  16925  pmtr3ncom  19450  efgmnvl  19689  efgrelexlema  19724  ring1ne0  20280  pzriprnglem8  21468  txuni2  23530  tx2ndc  23616  blssioo  24760  tgioo  24761  ioorf  25540  ioorinv  25543  ioorcl  25544  dyaddisj  25563  mbfid  25602  elply  26160  vmacl  27081  efvmacl  27083  vmalelog  27168  2sqlem2  27381  mul2sq  27382  2sqlem7  27387  2sqnn0  27401  2sqreultblem  27411  pntibnd  27556  ostth  27602  cutsf  27784  zaddscl  28386  zmulscld  28389  elzn0s  28390  eln0zs  28392  zseo  28414  elz12s  28464  z12no  28468  z12addscl  28469  z12shalf  28472  z12zsodd  28474  z12bdaylem  28476  bdayfinlem  28478  remulscllem1  28492  legval  28652  upgredgpr  29211  nbgr2vtx1edg  29419  cusgredg  29493  usgredgsscusgredg  29528  wwlksnwwlksnon  29983  n4cyclfrgr  30361  vdgn1frgrv2  30366  friendshipgt3  30468  lpni  30551  nsnlplig  30552  nsnlpligALT  30553  n0lpligALT  30555  ipasslem5  30906  ipasslem11  30911  hhssnv  31335  shscli  31388  shsleji  31441  shsidmi  31455  spansncvi  31723  superpos  32425  chirredi  32465  mdsymlem6  32479  rnmposs  32746  1fldgenq  33383  ccfldextdgrr  33816  cnre2csqima  34055  dya2icobrsiga  34420  dya2iocnrect  34425  dya2iocucvr  34428  sxbrsigalem2  34430  afsval  34815  satfv0  35540  satfrnmapom  35552  satfv0fun  35553  satf00  35556  sat1el2xp  35561  fmla0xp  35565  fmla1  35569  msubco  35713  elaltxp  36157  altxpsspw  36159  funtransport  36213  funray  36322  funline  36324  ellines  36334  linethru  36335  icoreresf  37668  icoreclin  37673  relowlssretop  37679  relowlpssretop  37680  itg2addnc  37995  isline  40185  sn-it0e0  42848  sn-mullid  42868  sn-0tie0  42896  sn-mul02  42897  mzpcompact2lem  43183  sprvalpw  47940  sprvalpwn0  47943  prsprel  47947  prpair  47961  prprvalpw  47975  reuopreuprim  47986  nnsum3primesgbe  48268  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  tgblthelfgott  48291  grtrif1o  48418  grtrissvtx  48420  gpgvtxel2  48524  pgn4cyclex  48602  nnpw2pb  49063  2arymaptf1  49129