Theorem rexlimivv 3199

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

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

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  r19.29vva  3213  2reu5  3754  2reu4  4526  opelxp  5712  elinxp  6019  reuop  6292  opiota  8047  f1o2ndf1  8110  poseq  8146  soseq  8147  tfrlem5  8382  xpdom2  9069  1sdomOLD  9251  unxpdomlem3  9254  unfiOLD  9315  elfiun  9427  ttrcltr  9713  xpnum  9948  kmlem9  10155  nqereu  10926  distrlem5pr  11024  mulrid  11214  1re  11216  mul02  11394  cnegex  11397  recex  11848  creur  12208  creui  12209  cju  12210  elz2  12578  zaddcl  12604  qre  12939  qaddcl  12951  qnegcl  12952  qmulcl  12953  qreccl  12955  elpqb  12962  hash2prd  14438  elss2prb  14450  fundmge2nop0  14455  wrdl3s3  14915  replim  15065  prodmo  15882  odd2np1  16286  opoe  16308  omoe  16309  opeo  16310  omeo  16311  qredeu  16597  pythagtriplem1  16751  pcz  16816  4sqlem1  16883  4sqlem2  16884  4sqlem4  16887  mul4sq  16889  pmtr3ncom  19345  efgmnvl  19584  efgrelexlema  19619  ring1ne0  20115  txuni2  23076  tx2ndc  23162  blssioo  24318  tgioo  24319  ioorf  25097  ioorinv  25100  ioorcl  25101  dyaddisj  25120  mbfid  25159  elply  25716  vmacl  26629  efvmacl  26631  vmalelog  26715  2sqlem2  26928  mul2sq  26929  2sqlem7  26934  2sqnn0  26948  2sqreultblem  26958  pntibnd  27103  ostth  27149  scutf  27321  legval  27873  upgredgpr  28440  nbgr2vtx1edg  28645  cusgredg  28719  usgredgsscusgredg  28754  wwlksnwwlksnon  29207  n4cyclfrgr  29582  vdgn1frgrv2  29587  friendshipgt3  29689  lpni  29771  nsnlplig  29772  nsnlpligALT  29773  n0lpligALT  29775  ipasslem5  30126  ipasslem11  30131  hhssnv  30555  shscli  30608  shsleji  30661  shsidmi  30675  spansncvi  30943  superpos  31645  chirredi  31685  mdsymlem6  31699  rnmposs  31937  1fldgenq  32453  ccfldextdgrr  32806  cnre2csqima  32960  dya2icobrsiga  33344  dya2iocnrect  33349  dya2iocucvr  33352  sxbrsigalem2  33354  afsval  33752  satfv0  34418  satfrnmapom  34430  satfv0fun  34431  satf00  34434  sat1el2xp  34439  fmla0xp  34443  fmla1  34447  msubco  34591  elaltxp  35016  altxpsspw  35018  funtransport  35072  funray  35181  funline  35183  ellines  35193  linethru  35194  icoreresf  36319  icoreclin  36324  relowlssretop  36330  relowlpssretop  36331  itg2addnc  36628  isline  38696  sn-it0e0  41370  sn-mullid  41390  sn-0tie0  41394  sn-mul02  41395  mzpcompact2lem  41571  sprvalpw  46227  sprvalpwn0  46230  prsprel  46234  prpair  46248  prprvalpw  46262  reuopreuprim  46273  nnsum3primesgbe  46539  nnsum4primesodd  46543  nnsum4primesoddALTV  46544  tgblthelfgott  46562  pzriprnglem8  46891  nnpw2pb  47351  2arymaptf1  47417