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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  r19.29vva  3222  2reu5  3780  2reu4  4546  opelxp  5736  elinxp  6048  reuop  6324  opiota  8100  f1o2ndf1  8163  poseq  8199  soseq  8200  tfrlem5  8436  xpdom2  9133  1sdomOLD  9312  unxpdomlem3  9315  elfiun  9499  ttrcltr  9785  xpnum  10020  kmlem9  10228  nqereu  10998  distrlem5pr  11096  mulrid  11288  1re  11290  mul02  11468  cnegex  11471  recex  11922  creur  12287  creui  12288  cju  12289  elz2  12657  zaddcl  12683  qre  13018  qaddcl  13030  qnegcl  13031  qmulcl  13032  qreccl  13034  elpqb  13041  hash2prd  14524  elss2prb  14537  fundmge2nop0  14551  wrdl3s3  15011  replim  15165  prodmo  15984  odd2np1  16389  opoe  16411  omoe  16412  opeo  16413  omeo  16414  qredeu  16705  pythagtriplem1  16863  pcz  16928  4sqlem1  16995  4sqlem2  16996  4sqlem4  16999  mul4sq  17001  pmtr3ncom  19517  efgmnvl  19756  efgrelexlema  19791  ring1ne0  20322  pzriprnglem8  21522  txuni2  23594  tx2ndc  23680  blssioo  24836  tgioo  24837  ioorf  25627  ioorinv  25630  ioorcl  25631  dyaddisj  25650  mbfid  25689  elply  26254  vmacl  27179  efvmacl  27181  vmalelog  27267  2sqlem2  27480  mul2sq  27481  2sqlem7  27486  2sqnn0  27500  2sqreultblem  27510  pntibnd  27655  ostth  27701  scutf  27875  zaddscl  28398  zmulscld  28401  elzn0s  28402  eln0zs  28404  zseo  28424  elzs12  28439  zs12bday  28442  remulscllem1  28450  legval  28610  upgredgpr  29177  nbgr2vtx1edg  29385  cusgredg  29459  usgredgsscusgredg  29495  wwlksnwwlksnon  29948  n4cyclfrgr  30323  vdgn1frgrv2  30328  friendshipgt3  30430  lpni  30512  nsnlplig  30513  nsnlpligALT  30514  n0lpligALT  30516  ipasslem5  30867  ipasslem11  30872  hhssnv  31296  shscli  31349  shsleji  31402  shsidmi  31416  spansncvi  31684  superpos  32386  chirredi  32426  mdsymlem6  32440  rnmposs  32692  1fldgenq  33289  ccfldextdgrr  33682  cnre2csqima  33857  dya2icobrsiga  34241  dya2iocnrect  34246  dya2iocucvr  34249  sxbrsigalem2  34251  afsval  34648  satfv0  35326  satfrnmapom  35338  satfv0fun  35339  satf00  35342  sat1el2xp  35347  fmla0xp  35351  fmla1  35355  msubco  35499  elaltxp  35939  altxpsspw  35941  funtransport  35995  funray  36104  funline  36106  ellines  36116  linethru  36117  icoreresf  37318  icoreclin  37323  relowlssretop  37329  relowlpssretop  37330  itg2addnc  37634  isline  39696  sn-it0e0  42391  sn-mullid  42411  sn-0tie0  42415  sn-mul02  42416  mzpcompact2lem  42707  sprvalpw  47354  sprvalpwn0  47357  prsprel  47361  prpair  47375  prprvalpw  47389  reuopreuprim  47400  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  tgblthelfgott  47689  grtrif1o  47793  grtrissvtx  47795  nnpw2pb  48321  2arymaptf1  48387