Theorem rexlimivv 3220

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  r19.29vva  3265  2reu5  3694  2reu4  4459  opelxp  5622  elinxp  5924  reuop  6191  opiota  7890  f1o2ndf1  7952  tfrlem5  8200  xpdom2  8843  1sdom  9014  unxpdomlem3  9018  unfiOLD  9070  elfiun  9178  ttrcltr  9463  xpnum  9698  kmlem9  9903  nqereu  10674  distrlem5pr  10772  mulid1  10962  1re  10964  mul02  11142  cnegex  11145  recex  11596  creur  11956  creui  11957  cju  11958  elz2  12326  zaddcl  12349  qre  12682  qaddcl  12694  qnegcl  12695  qmulcl  12696  qreccl  12698  elpqb  12705  hash2prd  14178  elss2prb  14190  fundmge2nop0  14195  wrdl3s3  14666  replim  14816  prodmo  15635  odd2np1  16039  opoe  16061  omoe  16062  opeo  16063  omeo  16064  qredeu  16352  pythagtriplem1  16506  pcz  16571  4sqlem1  16638  4sqlem2  16639  4sqlem4  16642  mul4sq  16644  pmtr3ncom  19072  efgmnvl  19309  efgrelexlema  19344  ring1ne0  19819  txuni2  22705  tx2ndc  22791  blssioo  23947  tgioo  23948  ioorf  24726  ioorinv  24729  ioorcl  24730  dyaddisj  24749  mbfid  24788  elply  25345  vmacl  26256  efvmacl  26258  vmalelog  26342  2sqlem2  26555  mul2sq  26556  2sqlem7  26561  2sqnn0  26575  2sqreultblem  26585  pntibnd  26730  ostth  26776  legval  26934  upgredgpr  27501  nbgr2vtx1edg  27706  cusgredg  27780  usgredgsscusgredg  27815  wwlksnwwlksnon  28267  n4cyclfrgr  28642  vdgn1frgrv2  28647  friendshipgt3  28749  lpni  28829  nsnlplig  28830  nsnlpligALT  28831  n0lpligALT  28833  ipasslem5  29184  ipasslem11  29189  hhssnv  29613  shscli  29666  shsleji  29719  shsidmi  29733  spansncvi  30001  superpos  30703  chirredi  30743  mdsymlem6  30757  rnmposs  30998  ccfldextdgrr  31729  cnre2csqima  31848  dya2icobrsiga  32230  dya2iocnrect  32235  dya2iocucvr  32238  sxbrsigalem2  32240  afsval  32638  satfv0  33307  satfrnmapom  33319  satfv0fun  33320  satf00  33323  sat1el2xp  33328  fmla0xp  33332  fmla1  33336  msubco  33480  poxp3  33783  poseq  33789  soseq  33790  scutf  33993  elaltxp  34264  altxpsspw  34266  funtransport  34320  funray  34429  funline  34431  ellines  34441  linethru  34442  icoreresf  35510  icoreclin  35515  relowlssretop  35521  relowlpssretop  35522  itg2addnc  35818  isline  37740  sn-it0e0  40384  sn-mulid2  40404  sn-0tie0  40408  sn-mul02  40409  mzpcompact2lem  40560  sprvalpw  44889  sprvalpwn0  44892  prsprel  44896  prpair  44910  prprvalpw  44924  reuopreuprim  44935  nnsum3primesgbe  45201  nnsum4primesodd  45205  nnsum4primesoddALTV  45206  tgblthelfgott  45224  nnpw2pb  45890  2arymaptf1  45956