Theorem rexlimivv 3208

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

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

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 1945

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

This theorem is used by:  r19.29vva  3226  2reu5  3719  2reu4  4483  opelxp  5694  elinxp  6026  reuop  6322  rnmposs  7586  opiota  8105  f1o2ndf1  8170  poseq  8212  soseq  8213  tfrlem5  8425  xpdom2  9129  unxpdomlem3  9287  elfiun  9459  ttrcltr  9754  xpnum  10069  kmlem9  10276  nqereu  11053  distrlem5pr  11151  mulrid  11345  1re  11347  mul02  11527  cnegex  11530  recex  11988  creur  12354  creui  12355  cju  12356  elz2  12751  zaddcl  12776  qre  13120  qaddcl  13133  qnegcl  13134  qmulcl  13135  qreccl  13137  elpqb  13144  hash2prd  14661  elss2prb  14674  fundmge2nop0  14688  s3rex  15144  wrdl3s3  15158  replim  15326  prodmo  16147  odd2np1  16555  opoe  16577  omoe  16578  opeo  16579  omeo  16580  qredeu  16877  pythagtriplem1  17038  pcz  17103  4sqlem1  17170  4sqlem2  17171  4sqlem4  17174  mul4sq  17176  pmtr3ncom  19740  efgmnvl  19979  efgrelexlema  20014  ring1ne0  20581  pzriprnglem8  21849  txuni2  23939  tx2ndc  24025  blssioo  25169  tgioo  25170  ioorf  25949  ioorinv  25952  ioorcl  25953  dyaddisj  25972  mbfid  26011  elply  26568  vmacl  27502  efvmacl  27504  vmalelog  27589  2sqlem2  27802  mul2sq  27803  2sqlem7  27808  2sqnn0  27822  2sqreultblem  27832  pntibnd  27977  ostth  28023  cutsf  28235  zaddscl  28837  zmulscld  28840  elzn0s  28841  eln0zs  28843  zseo  28865  elz12s  28915  z12no  28919  z12addscl  28920  z12shalf  28923  z12zsodd  28925  z12bdaylem  28927  bdayfinlem  28929  remulscllem1  28943  legval  29104  upgredgpr  29777  nbgr2vtx1edg  29988  cusgredg  30062  usgredgsscusgredg  30097  wwlksnwwlksnon  30561  n4cyclfrgr  30949  vdgn1frgrv2  30954  friendshipgt3  31056  lpni  31139  nsnlplig  31140  nsnlpligALT  31141  n0lpligALT  31143  ipasslem5  31494  ipasslem11  31499  hhssnv  31923  shscli  31976  shsleji  32029  shsidmi  32043  spansncvi  32311  superpos  33013  chirredi  33053  mdsymlem6  33067  1fldgenq  33988  ccfldextdgrr  34415  cnre2csqima  34654  dya2icobrsiga  35019  dya2iocnrect  35024  dya2iocucvr  35027  sxbrsigalem2  35029  afsval  35414  karddom  35970  kardsdom  35971  kardexen  35972  satfv0  36331  satfrnmapom  36343  satfv0fun  36344  satf00  36347  sat1el2xp  36352  fmla0xp  36356  fmla1  36360  msubco  36504  elaltxp  36955  altxpsspw  36957  funtransport  37011  funray  37120  funline  37122  ellines  37132  linethru  37133  icoreresf  38543  icoreclin  38548  relowlssretop  38554  relowlpssretop  38555  itg2addnc  38860  isline  41062  sn-it0e0  43733  sn-mullid  43753  sn-0tie0  43781  sn-mul02  43782  mzpcompact2lem  44028  sprvalpw  48835  sprvalpwn0  48838  prsprel  48842  prpair  48856  prprvalpw  48870  reuopreuprim  48881  nnsum3primesgbe  49163  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  tgblthelfgott  49186  grtrif1o  49313  grtrissvtx  49315  gpgvtxel2  49419  pgn4cyclex  49497  nnpw2pb  50030  2arymaptf1  50096