Theorem rexlimivv 3251

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∃wrex 3107

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  2reu5  3697  2reu4  4424  opelxp  5555  elinxp  5856  reuop  6112  opiota  7739  f1o2ndf1  7801  tfrlem5  7999  xpdom2  8595  1sdom  8705  unxpdomlem3  8708  unfi  8769  elfiun  8878  xpnum  9364  kmlem9  9569  nqereu  10340  distrlem5pr  10438  mulid1  10628  1re  10630  mul02  10807  cnegex  10810  recex  11261  creur  11619  creui  11620  cju  11621  elz2  11987  zaddcl  12010  qre  12341  qaddcl  12352  qnegcl  12353  qmulcl  12354  qreccl  12356  elpqb  12363  hash2prd  13829  elss2prb  13841  fundmge2nop0  13846  wrdl3s3  14317  replim  14467  prodmo  15282  odd2np1  15682  opoe  15704  omoe  15705  opeo  15706  omeo  15707  qredeu  15992  pythagtriplem1  16143  pcz  16207  4sqlem1  16274  4sqlem2  16275  4sqlem4  16278  mul4sq  16280  pmtr3ncom  18595  efgmnvl  18832  efgrelexlema  18867  ring1ne0  19337  txuni2  22170  tx2ndc  22256  blssioo  23400  tgioo  23401  ioorf  24177  ioorinv  24180  ioorcl  24181  dyaddisj  24200  mbfid  24239  elply  24792  vmacl  25703  efvmacl  25705  vmalelog  25789  2sqlem2  26002  mul2sq  26003  2sqlem7  26008  2sqnn0  26022  2sqreultblem  26032  pntibnd  26177  ostth  26223  legval  26378  upgredgpr  26935  nbgr2vtx1edg  27140  cusgredg  27214  usgredgsscusgredg  27249  wwlksnwwlksnon  27701  n4cyclfrgr  28076  vdgn1frgrv2  28081  friendshipgt3  28183  lpni  28263  nsnlplig  28264  nsnlpligALT  28265  n0lpligALT  28267  ipasslem5  28618  ipasslem11  28623  hhssnv  29047  shscli  29100  shsleji  29153  shsidmi  29167  spansncvi  29435  superpos  30137  chirredi  30177  mdsymlem6  30191  rnmposs  30437  ccfldextdgrr  31145  cnre2csqima  31264  dya2icobrsiga  31644  dya2iocnrect  31649  dya2iocucvr  31652  sxbrsigalem2  31654  afsval  32052  satfv0  32718  satfrnmapom  32730  satfv0fun  32731  satf00  32734  sat1el2xp  32739  fmla0xp  32743  fmla1  32747  msubco  32891  poseq  33208  soseq  33209  scutf  33386  elaltxp  33549  altxpsspw  33551  funtransport  33605  funray  33714  funline  33716  ellines  33726  linethru  33727  icoreresf  34769  icoreclin  34774  relowlssretop  34780  relowlpssretop  34781  itg2addnc  35111  isline  37035  sn-it0e0  39552  sn-mulid2  39572  sn-0tie0  39576  sn-mul02  39577  mzpcompact2lem  39692  sprvalpw  43997  sprvalpwn0  44000  prsprel  44004  prpair  44018  prprvalpw  44032  reuopreuprim  44043  nnsum3primesgbe  44310  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  tgblthelfgott  44333  nnpw2pb  45001  2arymaptf1  45067