Theorem rexlimivv 3292

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-ral 3143  df-rex 3144

This theorem is referenced by:  2reu5  3749  2reu4  4466  opelxp  5586  elinxp  5885  reuop  6139  opiota  7751  f1o2ndf1  7812  tfrlem5  8010  xpdom2  8606  1sdom  8715  unxpdomlem3  8718  unfi  8779  elfiun  8888  xpnum  9374  kmlem9  9578  nqereu  10345  distrlem5pr  10443  mulid1  10633  1re  10635  mul02  10812  cnegex  10815  recex  11266  creur  11626  creui  11627  cju  11628  elz2  11993  zaddcl  12016  qre  12347  qaddcl  12358  qnegcl  12359  qmulcl  12360  qreccl  12362  elpqb  12369  hash2prd  13827  elss2prb  13839  fundmge2nop0  13844  wrdl3s3  14320  replim  14469  prodmo  15284  odd2np1  15684  opoe  15706  omoe  15707  opeo  15708  omeo  15709  qredeu  15996  pythagtriplem1  16147  pcz  16211  4sqlem1  16278  4sqlem2  16279  4sqlem4  16282  mul4sq  16284  pmtr3ncom  18597  efgmnvl  18834  efgrelexlema  18869  ring1ne0  19335  txuni2  22167  tx2ndc  22253  blssioo  23397  tgioo  23398  ioorf  24168  ioorinv  24171  ioorcl  24172  dyaddisj  24191  mbfid  24230  elply  24779  vmacl  25689  efvmacl  25691  vmalelog  25775  2sqlem2  25988  mul2sq  25989  2sqlem7  25994  2sqnn0  26008  2sqreultblem  26018  pntibnd  26163  ostth  26209  legval  26364  upgredgpr  26921  nbgr2vtx1edg  27126  cusgredg  27200  usgredgsscusgredg  27235  wwlksnwwlksnon  27688  n4cyclfrgr  28064  vdgn1frgrv2  28069  friendshipgt3  28171  lpni  28251  nsnlplig  28252  nsnlpligALT  28253  n0lpligALT  28255  ipasslem5  28606  ipasslem11  28611  hhssnv  29035  shscli  29088  shsleji  29141  shsidmi  29155  spansncvi  29423  superpos  30125  chirredi  30165  mdsymlem6  30179  rnmposs  30413  ccfldextdgrr  31052  cnre2csqima  31149  dya2icobrsiga  31529  dya2iocnrect  31534  dya2iocucvr  31537  sxbrsigalem2  31539  afsval  31937  satfv0  32600  satfrnmapom  32612  satfv0fun  32613  satf00  32616  sat1el2xp  32621  fmla0xp  32625  fmla1  32629  msubco  32773  poseq  33090  soseq  33091  scutf  33268  elaltxp  33431  altxpsspw  33433  funtransport  33487  funray  33596  funline  33598  ellines  33608  linethru  33609  icoreresf  34627  icoreclin  34632  relowlssretop  34638  relowlpssretop  34639  itg2addnc  34940  isline  36869  mzpcompact2lem  39341  sprvalpw  43635  sprvalpwn0  43638  prsprel  43642  prpair  43656  prprvalpw  43670  reuopreuprim  43681  nnsum3primesgbe  43950  nnsum4primesodd  43954  nnsum4primesoddALTV  43955  tgblthelfgott  43973  nnpw2pb  44640