Theorem rexlimivv 3186

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3061

This theorem is referenced by:  r19.29vva  3201  2reu5  3741  2reu4  4498  opelxp  5690  elinxp  6006  reuop  6282  opiota  8056  f1o2ndf1  8119  poseq  8155  soseq  8156  tfrlem5  8392  xpdom2  9079  1sdomOLD  9255  unxpdomlem3  9258  elfiun  9440  ttrcltr  9728  xpnum  9963  kmlem9  10171  nqereu  10941  distrlem5pr  11039  mulrid  11231  1re  11233  mul02  11411  cnegex  11414  recex  11867  creur  12232  creui  12233  cju  12234  elz2  12604  zaddcl  12630  qre  12967  qaddcl  12979  qnegcl  12980  qmulcl  12981  qreccl  12983  elpqb  12990  hash2prd  14491  elss2prb  14504  fundmge2nop0  14518  wrdl3s3  14979  replim  15133  prodmo  15950  odd2np1  16358  opoe  16380  omoe  16381  opeo  16382  omeo  16383  qredeu  16675  pythagtriplem1  16834  pcz  16899  4sqlem1  16966  4sqlem2  16967  4sqlem4  16970  mul4sq  16972  pmtr3ncom  19454  efgmnvl  19693  efgrelexlema  19728  ring1ne0  20257  pzriprnglem8  21447  txuni2  23501  tx2ndc  23587  blssioo  24732  tgioo  24733  ioorf  25524  ioorinv  25527  ioorcl  25528  dyaddisj  25547  mbfid  25586  elply  26150  vmacl  27078  efvmacl  27080  vmalelog  27166  2sqlem2  27379  mul2sq  27380  2sqlem7  27385  2sqnn0  27399  2sqreultblem  27409  pntibnd  27554  ostth  27600  scutf  27774  zaddscl  28297  zmulscld  28300  elzn0s  28301  eln0zs  28303  zseo  28323  elzs12  28338  zs12bday  28341  remulscllem1  28349  legval  28509  upgredgpr  29067  nbgr2vtx1edg  29275  cusgredg  29349  usgredgsscusgredg  29385  wwlksnwwlksnon  29843  n4cyclfrgr  30218  vdgn1frgrv2  30223  friendshipgt3  30325  lpni  30407  nsnlplig  30408  nsnlpligALT  30409  n0lpligALT  30411  ipasslem5  30762  ipasslem11  30767  hhssnv  31191  shscli  31244  shsleji  31297  shsidmi  31311  spansncvi  31579  superpos  32281  chirredi  32321  mdsymlem6  32335  rnmposs  32598  1fldgenq  33262  ccfldextdgrr  33659  cnre2csqima  33888  dya2icobrsiga  34254  dya2iocnrect  34259  dya2iocucvr  34262  sxbrsigalem2  34264  afsval  34649  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  37316  icoreclin  37321  relowlssretop  37327  relowlpssretop  37328  itg2addnc  37644  isline  39704  sn-it0e0  42405  sn-mullid  42425  sn-0tie0  42429  sn-mul02  42430  mzpcompact2lem  42721  sprvalpw  47442  sprvalpwn0  47445  prsprel  47449  prpair  47463  prprvalpw  47477  reuopreuprim  47488  nnsum3primesgbe  47754  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  tgblthelfgott  47777  grtrif1o  47902  grtrissvtx  47904  gpgvtxel2  48000  nnpw2pb  48515  2arymaptf1  48581