Theorem rexlimivv 3221

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  r19.29vva  3266  2reu5  3693  2reu4  4457  opelxp  5625  elinxp  5929  reuop  6196  opiota  7899  f1o2ndf1  7963  tfrlem5  8211  xpdom2  8854  1sdom  9025  unxpdomlem3  9029  unfiOLD  9081  elfiun  9189  ttrcltr  9474  xpnum  9709  kmlem9  9914  nqereu  10685  distrlem5pr  10783  mulid1  10973  1re  10975  mul02  11153  cnegex  11156  recex  11607  creur  11967  creui  11968  cju  11969  elz2  12337  zaddcl  12360  qre  12693  qaddcl  12705  qnegcl  12706  qmulcl  12707  qreccl  12709  elpqb  12716  hash2prd  14189  elss2prb  14201  fundmge2nop0  14206  wrdl3s3  14677  replim  14827  prodmo  15646  odd2np1  16050  opoe  16072  omoe  16073  opeo  16074  omeo  16075  qredeu  16363  pythagtriplem1  16517  pcz  16582  4sqlem1  16649  4sqlem2  16650  4sqlem4  16653  mul4sq  16655  pmtr3ncom  19083  efgmnvl  19320  efgrelexlema  19355  ring1ne0  19830  txuni2  22716  tx2ndc  22802  blssioo  23958  tgioo  23959  ioorf  24737  ioorinv  24740  ioorcl  24741  dyaddisj  24760  mbfid  24799  elply  25356  vmacl  26267  efvmacl  26269  vmalelog  26353  2sqlem2  26566  mul2sq  26567  2sqlem7  26572  2sqnn0  26586  2sqreultblem  26596  pntibnd  26741  ostth  26787  legval  26945  upgredgpr  27512  nbgr2vtx1edg  27717  cusgredg  27791  usgredgsscusgredg  27826  wwlksnwwlksnon  28280  n4cyclfrgr  28655  vdgn1frgrv2  28660  friendshipgt3  28762  lpni  28842  nsnlplig  28843  nsnlpligALT  28844  n0lpligALT  28846  ipasslem5  29197  ipasslem11  29202  hhssnv  29626  shscli  29679  shsleji  29732  shsidmi  29746  spansncvi  30014  superpos  30716  chirredi  30756  mdsymlem6  30770  rnmposs  31011  ccfldextdgrr  31742  cnre2csqima  31861  dya2icobrsiga  32243  dya2iocnrect  32248  dya2iocucvr  32251  sxbrsigalem2  32253  afsval  32651  satfv0  33320  satfrnmapom  33332  satfv0fun  33333  satf00  33336  sat1el2xp  33341  fmla0xp  33345  fmla1  33349  msubco  33493  poxp3  33796  poseq  33802  soseq  33803  scutf  34006  elaltxp  34277  altxpsspw  34279  funtransport  34333  funray  34442  funline  34444  ellines  34454  linethru  34455  icoreresf  35523  icoreclin  35528  relowlssretop  35534  relowlpssretop  35535  itg2addnc  35831  isline  37753  sn-it0e0  40397  sn-mulid2  40417  sn-0tie0  40421  sn-mul02  40422  mzpcompact2lem  40573  sprvalpw  44932  sprvalpwn0  44935  prsprel  44939  prpair  44953  prprvalpw  44967  reuopreuprim  44978  nnsum3primesgbe  45244  nnsum4primesodd  45248  nnsum4primesoddALTV  45249  tgblthelfgott  45267  nnpw2pb  45933  2arymaptf1  45999