Theorem rexlimivv 3174

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  r19.29vva  3192  2reu5  3712  2reu4  4468  opelxp  5647  elinxp  5963  reuop  6235  opiota  7986  f1o2ndf1  8047  poseq  8083  soseq  8084  tfrlem5  8294  xpdom2  8980  unxpdomlem3  9137  elfiun  9309  ttrcltr  9601  xpnum  9839  kmlem9  10045  nqereu  10815  distrlem5pr  10913  mulrid  11105  1re  11107  mul02  11286  cnegex  11289  recex  11744  creur  12114  creui  12115  cju  12116  elz2  12481  zaddcl  12507  qre  12846  qaddcl  12858  qnegcl  12859  qmulcl  12860  qreccl  12862  elpqb  12869  hash2prd  14377  elss2prb  14390  fundmge2nop0  14404  wrdl3s3  14864  replim  15018  prodmo  15838  odd2np1  16247  opoe  16269  omoe  16270  opeo  16271  omeo  16272  qredeu  16564  pythagtriplem1  16723  pcz  16788  4sqlem1  16855  4sqlem2  16856  4sqlem4  16859  mul4sq  16861  pmtr3ncom  19382  efgmnvl  19621  efgrelexlema  19656  ring1ne0  20212  pzriprnglem8  21420  txuni2  23475  tx2ndc  23561  blssioo  24705  tgioo  24706  ioorf  25496  ioorinv  25499  ioorcl  25500  dyaddisj  25519  mbfid  25558  elply  26122  vmacl  27050  efvmacl  27052  vmalelog  27138  2sqlem2  27351  mul2sq  27352  2sqlem7  27357  2sqnn0  27371  2sqreultblem  27381  pntibnd  27526  ostth  27572  scutf  27748  zaddscl  28313  zmulscld  28316  elzn0s  28317  eln0zs  28319  zseo  28340  elzs12  28378  zs12no  28381  zs12addscl  28382  zs12half  28385  zs12zodd  28387  zs12bday  28389  remulscllem1  28397  legval  28557  upgredgpr  29115  nbgr2vtx1edg  29323  cusgredg  29397  usgredgsscusgredg  29433  wwlksnwwlksnon  29888  n4cyclfrgr  30263  vdgn1frgrv2  30268  friendshipgt3  30370  lpni  30452  nsnlplig  30453  nsnlpligALT  30454  n0lpligALT  30456  ipasslem5  30807  ipasslem11  30812  hhssnv  31236  shscli  31289  shsleji  31342  shsidmi  31356  spansncvi  31624  superpos  32326  chirredi  32366  mdsymlem6  32380  rnmposs  32648  1fldgenq  33280  ccfldextdgrr  33677  cnre2csqima  33916  dya2icobrsiga  34281  dya2iocnrect  34286  dya2iocucvr  34289  sxbrsigalem2  34291  afsval  34676  satfv0  35394  satfrnmapom  35406  satfv0fun  35407  satf00  35410  sat1el2xp  35415  fmla0xp  35419  fmla1  35423  msubco  35567  elaltxp  36009  altxpsspw  36011  funtransport  36065  funray  36174  funline  36176  ellines  36186  linethru  36187  icoreresf  37386  icoreclin  37391  relowlssretop  37397  relowlpssretop  37398  itg2addnc  37714  isline  39778  sn-it0e0  42449  sn-mullid  42469  sn-0tie0  42484  sn-mul02  42485  mzpcompact2lem  42784  sprvalpw  47511  sprvalpwn0  47514  prsprel  47518  prpair  47532  prprvalpw  47546  reuopreuprim  47557  nnsum3primesgbe  47823  nnsum4primesodd  47827  nnsum4primesoddALTV  47828  tgblthelfgott  47846  grtrif1o  47973  grtrissvtx  47975  gpgvtxel2  48079  pgn4cyclex  48157  nnpw2pb  48619  2arymaptf1  48685