Theorem rexlimivv 3190

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2099  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-rex 3061

This theorem is referenced by:  r19.29vva  3204  2reu5  3752  2reu4  4531  opelxp  5718  elinxp  6028  reuop  6304  opiota  8073  f1o2ndf1  8136  poseq  8172  soseq  8173  tfrlem5  8410  xpdom2  9105  1sdomOLD  9283  unxpdomlem3  9286  unfiOLD  9347  elfiun  9473  ttrcltr  9759  xpnum  9994  kmlem9  10201  nqereu  10972  distrlem5pr  11070  mulrid  11262  1re  11264  mul02  11442  cnegex  11445  recex  11896  creur  12258  creui  12259  cju  12260  elz2  12628  zaddcl  12654  qre  12989  qaddcl  13001  qnegcl  13002  qmulcl  13003  qreccl  13005  elpqb  13012  hash2prd  14494  elss2prb  14506  fundmge2nop0  14511  wrdl3s3  14971  replim  15121  prodmo  15938  odd2np1  16343  opoe  16365  omoe  16366  opeo  16367  omeo  16368  qredeu  16659  pythagtriplem1  16818  pcz  16883  4sqlem1  16950  4sqlem2  16951  4sqlem4  16954  mul4sq  16956  pmtr3ncom  19473  efgmnvl  19712  efgrelexlema  19747  ring1ne0  20278  pzriprnglem8  21478  txuni2  23560  tx2ndc  23646  blssioo  24802  tgioo  24803  ioorf  25593  ioorinv  25596  ioorcl  25597  dyaddisj  25616  mbfid  25655  elply  26222  vmacl  27146  efvmacl  27148  vmalelog  27234  2sqlem2  27447  mul2sq  27448  2sqlem7  27453  2sqnn0  27467  2sqreultblem  27477  pntibnd  27622  ostth  27668  scutf  27842  elzn0s  28342  remulscllem1  28351  legval  28511  upgredgpr  29078  nbgr2vtx1edg  29286  cusgredg  29360  usgredgsscusgredg  29396  wwlksnwwlksnon  29849  n4cyclfrgr  30224  vdgn1frgrv2  30229  friendshipgt3  30331  lpni  30413  nsnlplig  30414  nsnlpligALT  30415  n0lpligALT  30417  ipasslem5  30768  ipasslem11  30773  hhssnv  31197  shscli  31250  shsleji  31303  shsidmi  31317  spansncvi  31585  superpos  32287  chirredi  32327  mdsymlem6  32341  rnmposs  32591  1fldgenq  33172  ccfldextdgrr  33558  cnre2csqima  33726  dya2icobrsiga  34110  dya2iocnrect  34115  dya2iocucvr  34118  sxbrsigalem2  34120  afsval  34517  satfv0  35186  satfrnmapom  35198  satfv0fun  35199  satf00  35202  sat1el2xp  35207  fmla0xp  35211  fmla1  35215  msubco  35359  elaltxp  35799  altxpsspw  35801  funtransport  35855  funray  35964  funline  35966  ellines  35976  linethru  35977  icoreresf  37059  icoreclin  37064  relowlssretop  37070  relowlpssretop  37071  itg2addnc  37375  isline  39438  sn-it0e0  42195  sn-mullid  42215  sn-0tie0  42219  sn-mul02  42220  mzpcompact2lem  42408  sprvalpw  47052  sprvalpwn0  47055  prsprel  47059  prpair  47073  prprvalpw  47087  reuopreuprim  47098  nnsum3primesgbe  47364  nnsum4primesodd  47368  nnsum4primesoddALTV  47369  tgblthelfgott  47387  nnpw2pb  47975  2arymaptf1  48041