Theorem rexlimivv 3200

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

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 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  r19.29vva  3214  2reu5  3755  2reu4  4527  opelxp  5713  elinxp  6020  reuop  6293  opiota  8045  f1o2ndf1  8108  poseq  8144  soseq  8145  tfrlem5  8380  xpdom2  9067  1sdomOLD  9249  unxpdomlem3  9252  unfiOLD  9313  elfiun  9425  ttrcltr  9711  xpnum  9946  kmlem9  10153  nqereu  10924  distrlem5pr  11022  mulrid  11212  1re  11214  mul02  11392  cnegex  11395  recex  11846  creur  12206  creui  12207  cju  12208  elz2  12576  zaddcl  12602  qre  12937  qaddcl  12949  qnegcl  12950  qmulcl  12951  qreccl  12953  elpqb  12960  hash2prd  14436  elss2prb  14448  fundmge2nop0  14453  wrdl3s3  14913  replim  15063  prodmo  15880  odd2np1  16284  opoe  16306  omoe  16307  opeo  16308  omeo  16309  qredeu  16595  pythagtriplem1  16749  pcz  16814  4sqlem1  16881  4sqlem2  16882  4sqlem4  16885  mul4sq  16887  pmtr3ncom  19343  efgmnvl  19582  efgrelexlema  19617  ring1ne0  20111  txuni2  23069  tx2ndc  23155  blssioo  24311  tgioo  24312  ioorf  25090  ioorinv  25093  ioorcl  25094  dyaddisj  25113  mbfid  25152  elply  25709  vmacl  26622  efvmacl  26624  vmalelog  26708  2sqlem2  26921  mul2sq  26922  2sqlem7  26927  2sqnn0  26941  2sqreultblem  26951  pntibnd  27096  ostth  27142  scutf  27313  legval  27835  upgredgpr  28402  nbgr2vtx1edg  28607  cusgredg  28681  usgredgsscusgredg  28716  wwlksnwwlksnon  29169  n4cyclfrgr  29544  vdgn1frgrv2  29549  friendshipgt3  29651  lpni  29733  nsnlplig  29734  nsnlpligALT  29735  n0lpligALT  29737  ipasslem5  30088  ipasslem11  30093  hhssnv  30517  shscli  30570  shsleji  30623  shsidmi  30637  spansncvi  30905  superpos  31607  chirredi  31647  mdsymlem6  31661  rnmposs  31899  1fldgenq  32412  ccfldextdgrr  32746  cnre2csqima  32891  dya2icobrsiga  33275  dya2iocnrect  33280  dya2iocucvr  33283  sxbrsigalem2  33285  afsval  33683  satfv0  34349  satfrnmapom  34361  satfv0fun  34362  satf00  34365  sat1el2xp  34370  fmla0xp  34374  fmla1  34378  msubco  34522  elaltxp  34947  altxpsspw  34949  funtransport  35003  funray  35112  funline  35114  ellines  35124  linethru  35125  icoreresf  36233  icoreclin  36238  relowlssretop  36244  relowlpssretop  36245  itg2addnc  36542  isline  38610  sn-it0e0  41288  sn-mullid  41308  sn-0tie0  41312  sn-mul02  41313  mzpcompact2lem  41489  sprvalpw  46148  sprvalpwn0  46151  prsprel  46155  prpair  46169  prprvalpw  46183  reuopreuprim  46194  nnsum3primesgbe  46460  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  tgblthelfgott  46483  pzriprnglem8  46812  nnpw2pb  47273  2arymaptf1  47339