Theorem rexlimivv 3018

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  2reu5  3383  opelxp  5070  opiota  7118  f1o2ndf1  7172  tfrlem5  7363  xpdom2  7940  1sdom  8048  unxpdomlem3  8051  unfi  8112  elfiun  8219  xpnum  8660  kmlem9  8863  nqereu  9630  distrlem5pr  9728  mulid1  9916  1re  9918  mul02  10093  cnegex  10096  recex  10538  creur  10891  creui  10892  cju  10893  elz2  11271  zaddcl  11294  qre  11669  qaddcl  11680  qnegcl  11681  qmulcl  11682  qreccl  11684  hash2prd  13114  elss2prb  13123  fundmge2nop0  13129  wrdl3s3  13553  replim  13704  prodmo  14505  odd2np1  14903  opoe  14925  omoe  14926  opeo  14927  omeo  14928  qredeu  15210  pythagtriplem1  15359  pcz  15423  4sqlem1  15490  4sqlem2  15491  4sqlem4  15494  mul4sq  15496  pmtr3ncom  17718  efgmnvl  17950  efgrelexlema  17985  ring1ne0  18414  txuni2  21178  tx2ndc  21264  blssioo  22406  tgioo  22407  ioorf  23147  ioorinv  23150  ioorcl  23151  dyaddisj  23170  mbfid  23209  elply  23755  vmacl  24644  efvmacl  24646  vmalelog  24730  2sqlem2  24943  mul2sq  24944  2sqlem7  24949  pntibnd  25082  ostth  25128  legval  25279  upgredgpr  25815  usgrasscusgra  26011  el2wlksoton  26405  el2spthsoton  26406  n4cyclfrgra  26545  vdn0frgrav2  26550  vdgn0frgrav2  26551  vdn1frgrav2  26552  vdgn1frgrav2  26553  2spotmdisj  26595  friendshipgt3  26648  lpni  26722  ipasslem5  27074  ipasslem11  27079  hhssnv  27505  shscli  27560  shsleji  27613  shsidmi  27627  spansncvi  27895  superpos  28597  chirredi  28637  mdsymlem6  28651  rnmpt2ss  28856  cnre2csqima  29285  dya2icobrsiga  29665  dya2iocnrect  29670  dya2iocucvr  29673  sxbrsigalem2  29675  afsval  30002  msubco  30682  poseq  30994  soseq  30995  nofulllem5  31105  elaltxp  31252  altxpsspw  31254  funtransport  31308  funray  31417  funline  31419  ellines  31429  linethru  31430  icoreresf  32376  icoreclin  32381  relowlssretop  32387  relowlpssretop  32388  itg2addnc  32634  isline  34043  mzpcompact2lem  36332  2reu4  39839  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  tgblthelfgott  40229  nbgr2vtx1edg  40572  uvtx2vtx1edg  40625  cusgredg  40646  usgredgsscusgredg  40675  n4cyclfrgr  41461  vdgn1frgrv2  41466  av-friendshipgt3  41552  nnpw2pb  42179