Theorem rexlimivv 3213

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  r19.29vva  3231  2reu5  3730  2reu4  4490  opelxp  5698  elinxp  6019  reuop  6295  opiota  8055  f1o2ndf1  8116  poseq  8153  soseq  8154  tfrlem5  8365  xpdom2  9059  unxpdomlem3  9217  elfiun  9389  ttrcltr  9684  xpnum  9936  kmlem9  10141  nqereu  10913  distrlem5pr  11011  mulrid  11205  1re  11207  mul02  11387  cnegex  11390  recex  11845  creur  12211  creui  12212  cju  12213  elz2  12608  zaddcl  12633  qre  12976  qaddcl  12988  qnegcl  12989  qmulcl  12990  qreccl  12992  elpqb  12999  hash2prd  14511  elss2prb  14524  fundmge2nop0  14538  wrdl3s3  14998  replim  15166  prodmo  15989  odd2np1  16398  opoe  16420  omoe  16421  opeo  16422  omeo  16423  qredeu  16715  pythagtriplem1  16875  pcz  16940  4sqlem1  17007  4sqlem2  17008  4sqlem4  17011  mul4sq  17013  pmtr3ncom  19544  efgmnvl  19783  efgrelexlema  19818  ring1ne0  20381  pzriprnglem8  21606  txuni2  23690  tx2ndc  23776  blssioo  24920  tgioo  24921  ioorf  25700  ioorinv  25703  ioorcl  25704  dyaddisj  25723  mbfid  25762  elply  26320  vmacl  27247  efvmacl  27249  vmalelog  27334  2sqlem2  27547  mul2sq  27548  2sqlem7  27553  2sqnn0  27567  2sqreultblem  27577  pntibnd  27722  ostth  27768  cutsf  27950  zaddscl  28552  zmulscld  28555  elzn0s  28556  eln0zs  28558  zseo  28580  elz12s  28630  z12no  28634  z12addscl  28635  z12shalf  28638  z12zsodd  28640  z12bdaylem  28642  bdayfinlem  28644  remulscllem1  28658  legval  28818  upgredgpr  29432  nbgr2vtx1edg  29640  cusgredg  29714  usgredgsscusgredg  29749  wwlksnwwlksnon  30204  n4cyclfrgr  30582  vdgn1frgrv2  30587  friendshipgt3  30689  lpni  30772  nsnlplig  30773  nsnlpligALT  30774  n0lpligALT  30776  ipasslem5  31127  ipasslem11  31132  hhssnv  31556  shscli  31609  shsleji  31662  shsidmi  31676  spansncvi  31944  superpos  32646  chirredi  32686  mdsymlem6  32700  rnmposs  32958  1fldgenq  33585  ccfldextdgrr  34006  cnre2csqima  34245  dya2icobrsiga  34610  dya2iocnrect  34615  dya2iocucvr  34618  sxbrsigalem2  34620  afsval  35005  satfv0  35748  satfrnmapom  35760  satfv0fun  35761  satf00  35764  sat1el2xp  35769  fmla0xp  35773  fmla1  35777  msubco  35921  elaltxp  36365  altxpsspw  36367  funtransport  36421  funray  36530  funline  36532  ellines  36542  linethru  36543  icoreresf  37885  icoreclin  37890  relowlssretop  37896  relowlpssretop  37897  itg2addnc  38212  isline  40402  sn-it0e0  43066  sn-mullid  43086  sn-0tie0  43114  sn-mul02  43115  mzpcompact2lem  43373  sprvalpw  48117  sprvalpwn0  48120  prsprel  48124  prpair  48138  prprvalpw  48152  reuopreuprim  48163  nnsum3primesgbe  48445  nnsum4primesodd  48449  nnsum4primesoddALTV  48450  tgblthelfgott  48468  grtrif1o  48595  grtrissvtx  48597  gpgvtxel2  48701  pgn4cyclex  48779  nnpw2pb  49251  2arymaptf1  49317