Theorem rexlimivv 3175

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  r19.29vva  3193  2reu5  3713  2reu4  4474  opelxp  5657  elinxp  5975  reuop  6248  opiota  8000  f1o2ndf1  8061  poseq  8097  soseq  8098  tfrlem5  8308  xpdom2  8996  unxpdomlem3  9153  elfiun  9325  ttrcltr  9617  xpnum  9855  kmlem9  10061  nqereu  10831  distrlem5pr  10929  mulrid  11121  1re  11123  mul02  11302  cnegex  11305  recex  11760  creur  12130  creui  12131  cju  12132  elz2  12497  zaddcl  12522  qre  12857  qaddcl  12869  qnegcl  12870  qmulcl  12871  qreccl  12873  elpqb  12880  hash2prd  14389  elss2prb  14402  fundmge2nop0  14416  wrdl3s3  14876  replim  15030  prodmo  15850  odd2np1  16259  opoe  16281  omoe  16282  opeo  16283  omeo  16284  qredeu  16576  pythagtriplem1  16735  pcz  16800  4sqlem1  16867  4sqlem2  16868  4sqlem4  16871  mul4sq  16873  pmtr3ncom  19395  efgmnvl  19634  efgrelexlema  19669  ring1ne0  20225  pzriprnglem8  21434  txuni2  23500  tx2ndc  23586  blssioo  24730  tgioo  24731  ioorf  25521  ioorinv  25524  ioorcl  25525  dyaddisj  25544  mbfid  25583  elply  26147  vmacl  27075  efvmacl  27077  vmalelog  27163  2sqlem2  27376  mul2sq  27377  2sqlem7  27382  2sqnn0  27396  2sqreultblem  27406  pntibnd  27551  ostth  27597  scutf  27773  zaddscl  28338  zmulscld  28341  elzn0s  28342  eln0zs  28344  zseo  28365  elzs12  28403  zs12no  28406  zs12addscl  28407  zs12half  28410  zs12zodd  28412  zs12bday  28414  remulscllem1  28422  legval  28582  upgredgpr  29141  nbgr2vtx1edg  29349  cusgredg  29423  usgredgsscusgredg  29459  wwlksnwwlksnon  29914  n4cyclfrgr  30292  vdgn1frgrv2  30297  friendshipgt3  30399  lpni  30481  nsnlplig  30482  nsnlpligALT  30483  n0lpligALT  30485  ipasslem5  30836  ipasslem11  30841  hhssnv  31265  shscli  31318  shsleji  31371  shsidmi  31385  spansncvi  31653  superpos  32355  chirredi  32395  mdsymlem6  32409  rnmposs  32678  1fldgenq  33332  ccfldextdgrr  33757  cnre2csqima  33996  dya2icobrsiga  34361  dya2iocnrect  34366  dya2iocucvr  34369  sxbrsigalem2  34371  afsval  34756  satfv0  35474  satfrnmapom  35486  satfv0fun  35487  satf00  35490  sat1el2xp  35495  fmla0xp  35499  fmla1  35503  msubco  35647  elaltxp  36091  altxpsspw  36093  funtransport  36147  funray  36256  funline  36258  ellines  36268  linethru  36269  icoreresf  37469  icoreclin  37474  relowlssretop  37480  relowlpssretop  37481  itg2addnc  37787  isline  39911  sn-it0e0  42586  sn-mullid  42606  sn-0tie0  42621  sn-mul02  42622  mzpcompact2lem  42908  sprvalpw  47642  sprvalpwn0  47645  prsprel  47649  prpair  47663  prprvalpw  47677  reuopreuprim  47688  nnsum3primesgbe  47954  nnsum4primesodd  47958  nnsum4primesoddALTV  47959  tgblthelfgott  47977  grtrif1o  48104  grtrissvtx  48106  gpgvtxel2  48210  pgn4cyclex  48288  nnpw2pb  48749  2arymaptf1  48815