Theorem rexlimivv 3294

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∃wrex 3141

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 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  2reu5  3751  2reu4  4468  opelxp  5593  elinxp  5892  reuop  6146  opiota  7759  f1o2ndf1  7820  tfrlem5  8018  xpdom2  8614  1sdom  8723  unxpdomlem3  8726  unfi  8787  elfiun  8896  xpnum  9382  kmlem9  9586  nqereu  10353  distrlem5pr  10451  mulid1  10641  1re  10643  mul02  10820  cnegex  10823  recex  11274  creur  11634  creui  11635  cju  11636  elz2  12002  zaddcl  12025  qre  12356  qaddcl  12367  qnegcl  12368  qmulcl  12369  qreccl  12371  elpqb  12378  hash2prd  13836  elss2prb  13848  fundmge2nop0  13853  wrdl3s3  14328  replim  14477  prodmo  15292  odd2np1  15692  opoe  15714  omoe  15715  opeo  15716  omeo  15717  qredeu  16004  pythagtriplem1  16155  pcz  16219  4sqlem1  16286  4sqlem2  16287  4sqlem4  16290  mul4sq  16292  pmtr3ncom  18605  efgmnvl  18842  efgrelexlema  18877  ring1ne0  19343  txuni2  22175  tx2ndc  22261  blssioo  23405  tgioo  23406  ioorf  24176  ioorinv  24179  ioorcl  24180  dyaddisj  24199  mbfid  24238  elply  24787  vmacl  25697  efvmacl  25699  vmalelog  25783  2sqlem2  25996  mul2sq  25997  2sqlem7  26002  2sqnn0  26016  2sqreultblem  26026  pntibnd  26171  ostth  26217  legval  26372  upgredgpr  26929  nbgr2vtx1edg  27134  cusgredg  27208  usgredgsscusgredg  27243  wwlksnwwlksnon  27696  n4cyclfrgr  28072  vdgn1frgrv2  28077  friendshipgt3  28179  lpni  28259  nsnlplig  28260  nsnlpligALT  28261  n0lpligALT  28263  ipasslem5  28614  ipasslem11  28619  hhssnv  29043  shscli  29096  shsleji  29149  shsidmi  29163  spansncvi  29431  superpos  30133  chirredi  30173  mdsymlem6  30187  rnmposs  30421  ccfldextdgrr  31059  cnre2csqima  31156  dya2icobrsiga  31536  dya2iocnrect  31541  dya2iocucvr  31544  sxbrsigalem2  31546  afsval  31944  satfv0  32607  satfrnmapom  32619  satfv0fun  32620  satf00  32623  sat1el2xp  32628  fmla0xp  32632  fmla1  32636  msubco  32780  poseq  33097  soseq  33098  scutf  33275  elaltxp  33438  altxpsspw  33440  funtransport  33494  funray  33603  funline  33605  ellines  33615  linethru  33616  icoreresf  34635  icoreclin  34640  relowlssretop  34646  relowlpssretop  34647  itg2addnc  34948  isline  36877  mzpcompact2lem  39355  sprvalpw  43649  sprvalpwn0  43652  prsprel  43656  prpair  43670  prprvalpw  43684  reuopreuprim  43695  nnsum3primesgbe  43964  nnsum4primesodd  43968  nnsum4primesoddALTV  43969  tgblthelfgott  43987  nnpw2pb  44654