Theorem rexlimivv 3171

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  r19.29vva  3189  2reu5  3718  2reu4  4474  opelxp  5655  elinxp  5970  reuop  6241  opiota  7994  f1o2ndf1  8055  poseq  8091  soseq  8092  tfrlem5  8302  xpdom2  8989  unxpdomlem3  9147  elfiun  9320  ttrcltr  9612  xpnum  9847  kmlem9  10053  nqereu  10823  distrlem5pr  10921  mulrid  11113  1re  11115  mul02  11294  cnegex  11297  recex  11752  creur  12122  creui  12123  cju  12124  elz2  12489  zaddcl  12515  qre  12854  qaddcl  12866  qnegcl  12867  qmulcl  12868  qreccl  12870  elpqb  12877  hash2prd  14382  elss2prb  14395  fundmge2nop0  14409  wrdl3s3  14869  replim  15023  prodmo  15843  odd2np1  16252  opoe  16274  omoe  16275  opeo  16276  omeo  16277  qredeu  16569  pythagtriplem1  16728  pcz  16793  4sqlem1  16860  4sqlem2  16861  4sqlem4  16864  mul4sq  16866  pmtr3ncom  19354  efgmnvl  19593  efgrelexlema  19628  ring1ne0  20184  pzriprnglem8  21395  txuni2  23450  tx2ndc  23536  blssioo  24681  tgioo  24682  ioorf  25472  ioorinv  25475  ioorcl  25476  dyaddisj  25495  mbfid  25534  elply  26098  vmacl  27026  efvmacl  27028  vmalelog  27114  2sqlem2  27327  mul2sq  27328  2sqlem7  27333  2sqnn0  27347  2sqreultblem  27357  pntibnd  27502  ostth  27548  scutf  27723  zaddscl  28287  zmulscld  28290  elzn0s  28291  eln0zs  28293  zseo  28314  elzs12  28350  zs12no  28353  zs12addscl  28354  zs12half  28357  zs12zodd  28359  zs12bday  28361  remulscllem1  28369  legval  28529  upgredgpr  29087  nbgr2vtx1edg  29295  cusgredg  29369  usgredgsscusgredg  29405  wwlksnwwlksnon  29860  n4cyclfrgr  30235  vdgn1frgrv2  30240  friendshipgt3  30342  lpni  30424  nsnlplig  30425  nsnlpligALT  30426  n0lpligALT  30428  ipasslem5  30779  ipasslem11  30784  hhssnv  31208  shscli  31261  shsleji  31314  shsidmi  31328  spansncvi  31596  superpos  32298  chirredi  32338  mdsymlem6  32352  rnmposs  32617  1fldgenq  33261  ccfldextdgrr  33639  cnre2csqima  33878  dya2icobrsiga  34244  dya2iocnrect  34249  dya2iocucvr  34252  sxbrsigalem2  34254  afsval  34639  satfv0  35331  satfrnmapom  35343  satfv0fun  35344  satf00  35347  sat1el2xp  35352  fmla0xp  35356  fmla1  35360  msubco  35504  elaltxp  35949  altxpsspw  35951  funtransport  36005  funray  36114  funline  36116  ellines  36126  linethru  36127  icoreresf  37326  icoreclin  37331  relowlssretop  37337  relowlpssretop  37338  itg2addnc  37654  isline  39718  sn-it0e0  42389  sn-mullid  42409  sn-0tie0  42424  sn-mul02  42425  mzpcompact2lem  42724  sprvalpw  47464  sprvalpwn0  47467  prsprel  47471  prpair  47485  prprvalpw  47499  reuopreuprim  47510  nnsum3primesgbe  47776  nnsum4primesodd  47780  nnsum4primesoddALTV  47781  tgblthelfgott  47799  grtrif1o  47926  grtrissvtx  47928  gpgvtxel2  48032  pgn4cyclex  48110  nnpw2pb  48572  2arymaptf1  48638