Theorem rexlimivv 3204

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-rex 3087

This theorem is referenced by:  r19.29vva  3222  2reu5  3721  2reu4  4478  opelxp  5683  elinxp  6005  reuop  6280  opiota  8040  f1o2ndf1  8101  poseq  8138  soseq  8139  tfrlem5  8350  xpdom2  9044  unxpdomlem3  9202  elfiun  9376  ttrcltr  9671  xpnum  9909  kmlem9  10115  nqereu  10887  distrlem5pr  10985  mulrid  11179  1re  11181  mul02  11361  cnegex  11364  recex  11819  creur  12189  creui  12190  cju  12191  elz2  12586  zaddcl  12611  qre  12954  qaddcl  12966  qnegcl  12967  qmulcl  12968  qreccl  12970  elpqb  12977  hash2prd  14488  elss2prb  14501  fundmge2nop0  14515  wrdl3s3  14975  replim  15143  prodmo  15966  odd2np1  16375  opoe  16397  omoe  16398  opeo  16399  omeo  16400  qredeu  16692  pythagtriplem1  16852  pcz  16917  4sqlem1  16984  4sqlem2  16985  4sqlem4  16988  mul4sq  16990  pmtr3ncom  19515  efgmnvl  19754  efgrelexlema  19789  ring1ne0  20345  pzriprnglem8  21537  txuni2  23622  tx2ndc  23708  blssioo  24852  tgioo  24853  ioorf  25632  ioorinv  25635  ioorcl  25636  dyaddisj  25655  mbfid  25694  elply  26252  vmacl  27179  efvmacl  27181  vmalelog  27266  2sqlem2  27479  mul2sq  27480  2sqlem7  27485  2sqnn0  27499  2sqreultblem  27509  pntibnd  27654  ostth  27700  cutsf  27882  zaddscl  28484  zmulscld  28487  elzn0s  28488  eln0zs  28490  zseo  28512  elz12s  28562  z12no  28566  z12addscl  28567  z12shalf  28570  z12zsodd  28572  z12bdaylem  28574  bdayfinlem  28576  remulscllem1  28590  legval  28750  upgredgpr  29340  nbgr2vtx1edg  29548  cusgredg  29622  usgredgsscusgredg  29657  wwlksnwwlksnon  30112  n4cyclfrgr  30490  vdgn1frgrv2  30495  friendshipgt3  30597  lpni  30680  nsnlplig  30681  nsnlpligALT  30682  n0lpligALT  30684  ipasslem5  31035  ipasslem11  31040  hhssnv  31464  shscli  31517  shsleji  31570  shsidmi  31584  spansncvi  31852  superpos  32554  chirredi  32594  mdsymlem6  32608  rnmposs  32872  1fldgenq  33506  ccfldextdgrr  33966  cnre2csqima  34205  dya2icobrsiga  34570  dya2iocnrect  34575  dya2iocucvr  34578  sxbrsigalem2  34580  afsval  34965  satfv0  35705  satfrnmapom  35717  satfv0fun  35718  satf00  35721  sat1el2xp  35726  fmla0xp  35730  fmla1  35734  msubco  35878  elaltxp  36322  altxpsspw  36324  funtransport  36378  funray  36487  funline  36489  ellines  36499  linethru  36500  icoreresf  37843  icoreclin  37848  relowlssretop  37854  relowlpssretop  37855  itg2addnc  38170  isline  40360  sn-it0e0  43022  sn-mullid  43042  sn-0tie0  43070  sn-mul02  43071  mzpcompact2lem  43329  sprvalpw  48083  sprvalpwn0  48086  prsprel  48090  prpair  48104  prprvalpw  48118  reuopreuprim  48129  nnsum3primesgbe  48411  nnsum4primesodd  48415  nnsum4primesoddALTV  48416  tgblthelfgott  48434  grtrif1o  48561  grtrissvtx  48563  gpgvtxel2  48667  pgn4cyclex  48745  nnpw2pb  49206  2arymaptf1  49272