Theorem rexlimivv 3205

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  r19.29vva  3223  2reu5  3716  2reu4  4480  opelxp  5687  elinxp  6008  reuop  6295  opiota  8068  f1o2ndf1  8131  poseq  8168  soseq  8169  tfrlem5  8380  xpdom2  9084  unxpdomlem3  9242  elfiun  9415  ttrcltr  9710  xpnum  10025  kmlem9  10230  nqereu  11007  distrlem5pr  11105  mulrid  11299  1re  11301  mul02  11481  cnegex  11484  recex  11941  creur  12307  creui  12308  cju  12309  elz2  12704  zaddcl  12729  qre  13073  qaddcl  13086  qnegcl  13087  qmulcl  13088  qreccl  13090  elpqb  13097  hash2prd  14613  elss2prb  14626  fundmge2nop0  14640  s3rex  15094  wrdl3s3  15108  replim  15276  prodmo  16096  odd2np1  16504  opoe  16526  omoe  16527  opeo  16528  omeo  16529  qredeu  16826  pythagtriplem1  16987  pcz  17052  4sqlem1  17119  4sqlem2  17120  4sqlem4  17123  mul4sq  17125  pmtr3ncom  19682  efgmnvl  19921  efgrelexlema  19956  ring1ne0  20523  pzriprnglem8  21787  txuni2  23877  tx2ndc  23963  blssioo  25107  tgioo  25108  ioorf  25887  ioorinv  25890  ioorcl  25891  dyaddisj  25910  mbfid  25949  elply  26506  vmacl  27438  efvmacl  27440  vmalelog  27525  2sqlem2  27738  mul2sq  27739  2sqlem7  27744  2sqnn0  27758  2sqreultblem  27768  pntibnd  27913  ostth  27959  cutsf  28171  zaddscl  28773  zmulscld  28776  elzn0s  28777  eln0zs  28779  zseo  28801  elz12s  28851  z12no  28855  z12addscl  28856  z12shalf  28859  z12zsodd  28861  z12bdaylem  28863  bdayfinlem  28865  remulscllem1  28879  legval  29040  upgredgpr  29713  nbgr2vtx1edg  29924  cusgredg  29998  usgredgsscusgredg  30033  wwlksnwwlksnon  30497  n4cyclfrgr  30885  vdgn1frgrv2  30890  friendshipgt3  30992  lpni  31075  nsnlplig  31076  nsnlpligALT  31077  n0lpligALT  31079  ipasslem5  31430  ipasslem11  31435  hhssnv  31859  shscli  31912  shsleji  31965  shsidmi  31979  spansncvi  32247  superpos  32949  chirredi  32989  mdsymlem6  33003  rnmposs  33260  1fldgenq  33877  ccfldextdgrr  34297  cnre2csqima  34536  dya2icobrsiga  34901  dya2iocnrect  34906  dya2iocucvr  34909  sxbrsigalem2  34911  afsval  35296  karddom  35812  kardsdom  35813  kardexen  35814  satfv0  36102  satfrnmapom  36114  satfv0fun  36115  satf00  36118  sat1el2xp  36123  fmla0xp  36127  fmla1  36131  msubco  36275  elaltxp  36720  altxpsspw  36722  funtransport  36776  funray  36885  funline  36887  ellines  36897  linethru  36898  icoreresf  38255  icoreclin  38260  relowlssretop  38266  relowlpssretop  38267  itg2addnc  38572  isline  40776  sn-it0e0  43447  sn-mullid  43467  sn-0tie0  43495  sn-mul02  43496  mzpcompact2lem  43741  sprvalpw  48531  sprvalpwn0  48534  prsprel  48538  prpair  48552  prprvalpw  48566  reuopreuprim  48577  nnsum3primesgbe  48859  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  tgblthelfgott  48882  grtrif1o  49009  grtrissvtx  49011  gpgvtxel2  49115  pgn4cyclex  49193  nnpw2pb  49668  2arymaptf1  49734