Theorem rexlimivv 3184

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-rex 3060

This theorem is referenced by:  r19.29vva  3199  2reu5  3739  2reu4  4496  opelxp  5688  elinxp  6004  reuop  6280  opiota  8053  f1o2ndf1  8116  poseq  8152  soseq  8153  tfrlem5  8389  xpdom2  9076  1sdomOLD  9252  unxpdomlem3  9255  elfiun  9437  ttrcltr  9723  xpnum  9958  kmlem9  10166  nqereu  10936  distrlem5pr  11034  mulrid  11226  1re  11228  mul02  11406  cnegex  11409  recex  11862  creur  12227  creui  12228  cju  12229  elz2  12599  zaddcl  12625  qre  12962  qaddcl  12974  qnegcl  12975  qmulcl  12976  qreccl  12978  elpqb  12985  hash2prd  14483  elss2prb  14496  fundmge2nop0  14510  wrdl3s3  14970  replim  15124  prodmo  15941  odd2np1  16347  opoe  16369  omoe  16370  opeo  16371  omeo  16372  qredeu  16664  pythagtriplem1  16823  pcz  16888  4sqlem1  16955  4sqlem2  16956  4sqlem4  16959  mul4sq  16961  pmtr3ncom  19443  efgmnvl  19682  efgrelexlema  19717  ring1ne0  20246  pzriprnglem8  21436  txuni2  23490  tx2ndc  23576  blssioo  24721  tgioo  24722  ioorf  25513  ioorinv  25516  ioorcl  25517  dyaddisj  25536  mbfid  25575  elply  26139  vmacl  27066  efvmacl  27068  vmalelog  27154  2sqlem2  27367  mul2sq  27368  2sqlem7  27373  2sqnn0  27387  2sqreultblem  27397  pntibnd  27542  ostth  27588  scutf  27762  zaddscl  28285  zmulscld  28288  elzn0s  28289  eln0zs  28291  zseo  28311  elzs12  28326  zs12bday  28329  remulscllem1  28337  legval  28497  upgredgpr  29055  nbgr2vtx1edg  29263  cusgredg  29337  usgredgsscusgredg  29373  wwlksnwwlksnon  29831  n4cyclfrgr  30206  vdgn1frgrv2  30211  friendshipgt3  30313  lpni  30395  nsnlplig  30396  nsnlpligALT  30397  n0lpligALT  30399  ipasslem5  30750  ipasslem11  30755  hhssnv  31179  shscli  31232  shsleji  31285  shsidmi  31299  spansncvi  31567  superpos  32269  chirredi  32309  mdsymlem6  32323  rnmposs  32586  1fldgenq  33253  ccfldextdgrr  33648  cnre2csqima  33871  dya2icobrsiga  34237  dya2iocnrect  34242  dya2iocucvr  34245  sxbrsigalem2  34247  afsval  34632  satfv0  35309  satfrnmapom  35321  satfv0fun  35322  satf00  35325  sat1el2xp  35330  fmla0xp  35334  fmla1  35338  msubco  35482  elaltxp  35922  altxpsspw  35924  funtransport  35978  funray  36087  funline  36089  ellines  36099  linethru  36100  icoreresf  37299  icoreclin  37304  relowlssretop  37310  relowlpssretop  37311  itg2addnc  37627  isline  39687  sn-it0e0  42390  sn-mullid  42410  sn-0tie0  42414  sn-mul02  42415  mzpcompact2lem  42706  sprvalpw  47420  sprvalpwn0  47423  prsprel  47427  prpair  47441  prprvalpw  47455  reuopreuprim  47466  nnsum3primesgbe  47732  nnsum4primesodd  47736  nnsum4primesoddALTV  47737  tgblthelfgott  47755  grtrif1o  47862  grtrissvtx  47864  gpgvtxel2  47959  nnpw2pb  48461  2arymaptf1  48527