Theorem rexlimivv 3201

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 395   ∈ wcel 2108  ∃wrex 3070

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 3071

This theorem is referenced by:  r19.29vva  3216  2reu5  3764  2reu4  4523  opelxp  5721  elinxp  6037  reuop  6313  opiota  8084  f1o2ndf1  8147  poseq  8183  soseq  8184  tfrlem5  8420  xpdom2  9107  1sdomOLD  9285  unxpdomlem3  9288  elfiun  9470  ttrcltr  9756  xpnum  9991  kmlem9  10199  nqereu  10969  distrlem5pr  11067  mulrid  11259  1re  11261  mul02  11439  cnegex  11442  recex  11895  creur  12260  creui  12261  cju  12262  elz2  12631  zaddcl  12657  qre  12995  qaddcl  13007  qnegcl  13008  qmulcl  13009  qreccl  13011  elpqb  13018  hash2prd  14514  elss2prb  14527  fundmge2nop0  14541  wrdl3s3  15001  replim  15155  prodmo  15972  odd2np1  16378  opoe  16400  omoe  16401  opeo  16402  omeo  16403  qredeu  16695  pythagtriplem1  16854  pcz  16919  4sqlem1  16986  4sqlem2  16987  4sqlem4  16990  mul4sq  16992  pmtr3ncom  19493  efgmnvl  19732  efgrelexlema  19767  ring1ne0  20296  pzriprnglem8  21499  txuni2  23573  tx2ndc  23659  blssioo  24816  tgioo  24817  ioorf  25608  ioorinv  25611  ioorcl  25612  dyaddisj  25631  mbfid  25670  elply  26234  vmacl  27161  efvmacl  27163  vmalelog  27249  2sqlem2  27462  mul2sq  27463  2sqlem7  27468  2sqnn0  27482  2sqreultblem  27492  pntibnd  27637  ostth  27683  scutf  27857  zaddscl  28380  zmulscld  28383  elzn0s  28384  eln0zs  28386  zseo  28406  elzs12  28421  zs12bday  28424  remulscllem1  28432  legval  28592  upgredgpr  29159  nbgr2vtx1edg  29367  cusgredg  29441  usgredgsscusgredg  29477  wwlksnwwlksnon  29935  n4cyclfrgr  30310  vdgn1frgrv2  30315  friendshipgt3  30417  lpni  30499  nsnlplig  30500  nsnlpligALT  30501  n0lpligALT  30503  ipasslem5  30854  ipasslem11  30859  hhssnv  31283  shscli  31336  shsleji  31389  shsidmi  31403  spansncvi  31671  superpos  32373  chirredi  32413  mdsymlem6  32427  rnmposs  32684  1fldgenq  33324  ccfldextdgrr  33722  cnre2csqima  33910  dya2icobrsiga  34278  dya2iocnrect  34283  dya2iocucvr  34286  sxbrsigalem2  34288  afsval  34686  satfv0  35363  satfrnmapom  35375  satfv0fun  35376  satf00  35379  sat1el2xp  35384  fmla0xp  35388  fmla1  35392  msubco  35536  elaltxp  35976  altxpsspw  35978  funtransport  36032  funray  36141  funline  36143  ellines  36153  linethru  36154  icoreresf  37353  icoreclin  37358  relowlssretop  37364  relowlpssretop  37365  itg2addnc  37681  isline  39741  sn-it0e0  42445  sn-mullid  42465  sn-0tie0  42469  sn-mul02  42470  mzpcompact2lem  42762  sprvalpw  47467  sprvalpwn0  47470  prsprel  47474  prpair  47488  prprvalpw  47502  reuopreuprim  47513  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  tgblthelfgott  47802  grtrif1o  47909  grtrissvtx  47911  gpgvtxel2  48006  nnpw2pb  48508  2arymaptf1  48574