Theorem rexlimivv 3177

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  r19.29vva  3195  2reu5  3726  2reu4  4482  opelxp  5667  elinxp  5979  reuop  6254  opiota  8017  f1o2ndf1  8078  poseq  8114  soseq  8115  tfrlem5  8325  xpdom2  9013  1sdomOLD  9172  unxpdomlem3  9175  elfiun  9357  ttrcltr  9645  xpnum  9880  kmlem9  10088  nqereu  10858  distrlem5pr  10956  mulrid  11148  1re  11150  mul02  11328  cnegex  11331  recex  11786  creur  12156  creui  12157  cju  12158  elz2  12523  zaddcl  12549  qre  12888  qaddcl  12900  qnegcl  12901  qmulcl  12902  qreccl  12904  elpqb  12911  hash2prd  14416  elss2prb  14429  fundmge2nop0  14443  wrdl3s3  14904  replim  15058  prodmo  15878  odd2np1  16287  opoe  16309  omoe  16310  opeo  16311  omeo  16312  qredeu  16604  pythagtriplem1  16763  pcz  16828  4sqlem1  16895  4sqlem2  16896  4sqlem4  16899  mul4sq  16901  pmtr3ncom  19381  efgmnvl  19620  efgrelexlema  19655  ring1ne0  20184  pzriprnglem8  21374  txuni2  23428  tx2ndc  23514  blssioo  24659  tgioo  24660  ioorf  25450  ioorinv  25453  ioorcl  25454  dyaddisj  25473  mbfid  25512  elply  26076  vmacl  27004  efvmacl  27006  vmalelog  27092  2sqlem2  27305  mul2sq  27306  2sqlem7  27311  2sqnn0  27325  2sqreultblem  27335  pntibnd  27480  ostth  27526  scutf  27700  zaddscl  28258  zmulscld  28261  elzn0s  28262  eln0zs  28264  zseo  28284  elzs12  28313  zs12bday  28319  remulscllem1  28327  legval  28487  upgredgpr  29045  nbgr2vtx1edg  29253  cusgredg  29327  usgredgsscusgredg  29363  wwlksnwwlksnon  29818  n4cyclfrgr  30193  vdgn1frgrv2  30198  friendshipgt3  30300  lpni  30382  nsnlplig  30383  nsnlpligALT  30384  n0lpligALT  30386  ipasslem5  30737  ipasslem11  30742  hhssnv  31166  shscli  31219  shsleji  31272  shsidmi  31286  spansncvi  31554  superpos  32256  chirredi  32296  mdsymlem6  32310  rnmposs  32571  1fldgenq  33245  ccfldextdgrr  33640  cnre2csqima  33874  dya2icobrsiga  34240  dya2iocnrect  34245  dya2iocucvr  34248  sxbrsigalem2  34250  afsval  34635  satfv0  35318  satfrnmapom  35330  satfv0fun  35331  satf00  35334  sat1el2xp  35339  fmla0xp  35343  fmla1  35347  msubco  35491  elaltxp  35936  altxpsspw  35938  funtransport  35992  funray  36101  funline  36103  ellines  36113  linethru  36114  icoreresf  37313  icoreclin  37318  relowlssretop  37324  relowlpssretop  37325  itg2addnc  37641  isline  39706  sn-it0e0  42377  sn-mullid  42397  sn-0tie0  42412  sn-mul02  42413  mzpcompact2lem  42712  sprvalpw  47454  sprvalpwn0  47457  prsprel  47461  prpair  47475  prprvalpw  47489  reuopreuprim  47500  nnsum3primesgbe  47766  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  tgblthelfgott  47789  grtrif1o  47914  grtrissvtx  47916  gpgvtxel2  48012  pgn4cyclex  48089  nnpw2pb  48549  2arymaptf1  48615