Theorem rexlimivv 3207

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  r19.29vva  3225  2reu5  3721  2reu4  4485  opelxp  5697  elinxp  6018  reuop  6294  opiota  8052  f1o2ndf1  8113  poseq  8150  soseq  8151  tfrlem5  8362  xpdom2  9056  unxpdomlem3  9214  elfiun  9386  ttrcltr  9681  xpnum  9933  kmlem9  10138  nqereu  10909  distrlem5pr  11007  mulrid  11201  1re  11203  mul02  11383  cnegex  11386  recex  11841  creur  12207  creui  12208  cju  12209  elz2  12604  zaddcl  12629  qre  12972  qaddcl  12984  qnegcl  12985  qmulcl  12986  qreccl  12988  elpqb  12995  hash2prd  14508  elss2prb  14521  fundmge2nop0  14535  wrdl3s3  14995  replim  15163  prodmo  15986  odd2np1  16394  opoe  16416  omoe  16417  opeo  16418  omeo  16419  qredeu  16711  pythagtriplem1  16871  pcz  16936  4sqlem1  17003  4sqlem2  17004  4sqlem4  17007  mul4sq  17009  pmtr3ncom  19540  efgmnvl  19779  efgrelexlema  19814  ring1ne0  20378  pzriprnglem8  21638  txuni2  23722  tx2ndc  23808  blssioo  24952  tgioo  24953  ioorf  25732  ioorinv  25735  ioorcl  25736  dyaddisj  25755  mbfid  25794  elply  26352  vmacl  27282  efvmacl  27284  vmalelog  27369  2sqlem2  27582  mul2sq  27583  2sqlem7  27588  2sqnn0  27602  2sqreultblem  27612  pntibnd  27757  ostth  27803  cutsf  27985  zaddscl  28587  zmulscld  28590  elzn0s  28591  eln0zs  28593  zseo  28615  elz12s  28665  z12no  28669  z12addscl  28670  z12shalf  28673  z12zsodd  28675  z12bdaylem  28677  bdayfinlem  28679  remulscllem1  28693  legval  28853  upgredgpr  29492  nbgr2vtx1edg  29700  cusgredg  29774  usgredgsscusgredg  29809  wwlksnwwlksnon  30264  n4cyclfrgr  30642  vdgn1frgrv2  30647  friendshipgt3  30749  lpni  30832  nsnlplig  30833  nsnlpligALT  30834  n0lpligALT  30836  ipasslem5  31187  ipasslem11  31192  hhssnv  31616  shscli  31669  shsleji  31722  shsidmi  31736  spansncvi  32004  superpos  32706  chirredi  32746  mdsymlem6  32760  rnmposs  33018  1fldgenq  33643  ccfldextdgrr  34062  cnre2csqima  34301  dya2icobrsiga  34666  dya2iocnrect  34671  dya2iocucvr  34674  sxbrsigalem2  34676  afsval  35061  karddom  35574  kardsdom  35575  kardexen  35576  satfv0  35850  satfrnmapom  35862  satfv0fun  35863  satf00  35866  sat1el2xp  35871  fmla0xp  35875  fmla1  35879  msubco  36023  elaltxp  36467  altxpsspw  36469  funtransport  36523  funray  36632  funline  36634  ellines  36644  linethru  36645  icoreresf  37998  icoreclin  38003  relowlssretop  38009  relowlpssretop  38010  itg2addnc  38325  isline  40513  sn-it0e0  43177  sn-mullid  43197  sn-0tie0  43225  sn-mul02  43226  mzpcompact2lem  43482  sprvalpw  48229  sprvalpwn0  48232  prsprel  48236  prpair  48250  prprvalpw  48264  reuopreuprim  48275  nnsum3primesgbe  48557  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  tgblthelfgott  48580  grtrif1o  48707  grtrissvtx  48709  gpgvtxel2  48813  pgn4cyclex  48891  nnpw2pb  49367  2arymaptf1  49433