Theorem rexlimivv 3198

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  r19.29vva  3213  2reu5  3766  2reu4  4528  opelxp  5724  elinxp  6038  reuop  6314  opiota  8082  f1o2ndf1  8145  poseq  8181  soseq  8182  tfrlem5  8418  xpdom2  9105  1sdomOLD  9282  unxpdomlem3  9285  elfiun  9467  ttrcltr  9753  xpnum  9988  kmlem9  10196  nqereu  10966  distrlem5pr  11064  mulrid  11256  1re  11258  mul02  11436  cnegex  11439  recex  11892  creur  12257  creui  12258  cju  12259  elz2  12628  zaddcl  12654  qre  12992  qaddcl  13004  qnegcl  13005  qmulcl  13006  qreccl  13008  elpqb  13015  hash2prd  14510  elss2prb  14523  fundmge2nop0  14537  wrdl3s3  14997  replim  15151  prodmo  15968  odd2np1  16374  opoe  16396  omoe  16397  opeo  16398  omeo  16399  qredeu  16691  pythagtriplem1  16849  pcz  16914  4sqlem1  16981  4sqlem2  16982  4sqlem4  16985  mul4sq  16987  pmtr3ncom  19507  efgmnvl  19746  efgrelexlema  19781  ring1ne0  20312  pzriprnglem8  21516  txuni2  23588  tx2ndc  23674  blssioo  24830  tgioo  24831  ioorf  25621  ioorinv  25624  ioorcl  25625  dyaddisj  25644  mbfid  25683  elply  26248  vmacl  27175  efvmacl  27177  vmalelog  27263  2sqlem2  27476  mul2sq  27477  2sqlem7  27482  2sqnn0  27496  2sqreultblem  27506  pntibnd  27651  ostth  27697  scutf  27871  zaddscl  28394  zmulscld  28397  elzn0s  28398  eln0zs  28400  zseo  28420  elzs12  28435  zs12bday  28438  remulscllem1  28446  legval  28606  upgredgpr  29173  nbgr2vtx1edg  29381  cusgredg  29455  usgredgsscusgredg  29491  wwlksnwwlksnon  29944  n4cyclfrgr  30319  vdgn1frgrv2  30324  friendshipgt3  30426  lpni  30508  nsnlplig  30509  nsnlpligALT  30510  n0lpligALT  30512  ipasslem5  30863  ipasslem11  30868  hhssnv  31292  shscli  31345  shsleji  31398  shsidmi  31412  spansncvi  31680  superpos  32382  chirredi  32422  mdsymlem6  32436  rnmposs  32690  1fldgenq  33303  ccfldextdgrr  33696  cnre2csqima  33871  dya2icobrsiga  34257  dya2iocnrect  34262  dya2iocucvr  34265  sxbrsigalem2  34267  afsval  34664  satfv0  35342  satfrnmapom  35354  satfv0fun  35355  satf00  35358  sat1el2xp  35363  fmla0xp  35367  fmla1  35371  msubco  35515  elaltxp  35956  altxpsspw  35958  funtransport  36012  funray  36121  funline  36123  ellines  36133  linethru  36134  icoreresf  37334  icoreclin  37339  relowlssretop  37345  relowlpssretop  37346  itg2addnc  37660  isline  39721  sn-it0e0  42421  sn-mullid  42441  sn-0tie0  42445  sn-mul02  42446  mzpcompact2lem  42738  sprvalpw  47404  sprvalpwn0  47407  prsprel  47411  prpair  47425  prprvalpw  47439  reuopreuprim  47450  nnsum3primesgbe  47716  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  tgblthelfgott  47739  grtrif1o  47846  grtrissvtx  47848  gpgvtxel2  47941  nnpw2pb  48436  2arymaptf1  48502