Theorem rexlimivv 3204

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  r19.29vva  3222  2reu5  3715  2reu4  4479  opelxp  5687  elinxp  6010  reuop  6299  opiota  8074  f1o2ndf1  8139  poseq  8181  soseq  8182  tfrlem5  8394  xpdom2  9098  unxpdomlem3  9256  elfiun  9429  ttrcltr  9724  xpnum  10039  kmlem9  10244  nqereu  11021  distrlem5pr  11119  mulrid  11313  1re  11315  mul02  11495  cnegex  11498  recex  11955  creur  12321  creui  12322  cju  12323  elz2  12718  zaddcl  12743  qre  13087  qaddcl  13100  qnegcl  13101  qmulcl  13102  qreccl  13104  elpqb  13111  hash2prd  14627  elss2prb  14640  fundmge2nop0  14654  s3rex  15110  wrdl3s3  15124  replim  15292  prodmo  16112  odd2np1  16520  opoe  16542  omoe  16543  opeo  16544  omeo  16545  qredeu  16842  pythagtriplem1  17003  pcz  17068  4sqlem1  17135  4sqlem2  17136  4sqlem4  17139  mul4sq  17141  pmtr3ncom  19698  efgmnvl  19937  efgrelexlema  19972  ring1ne0  20539  pzriprnglem8  21803  txuni2  23893  tx2ndc  23979  blssioo  25123  tgioo  25124  ioorf  25903  ioorinv  25906  ioorcl  25907  dyaddisj  25926  mbfid  25965  elply  26522  vmacl  27454  efvmacl  27456  vmalelog  27541  2sqlem2  27754  mul2sq  27755  2sqlem7  27760  2sqnn0  27774  2sqreultblem  27784  pntibnd  27929  ostth  27975  cutsf  28187  zaddscl  28789  zmulscld  28792  elzn0s  28793  eln0zs  28795  zseo  28817  elz12s  28867  z12no  28871  z12addscl  28872  z12shalf  28875  z12zsodd  28877  z12bdaylem  28879  bdayfinlem  28881  remulscllem1  28895  legval  29056  upgredgpr  29729  nbgr2vtx1edg  29940  cusgredg  30014  usgredgsscusgredg  30049  wwlksnwwlksnon  30513  n4cyclfrgr  30901  vdgn1frgrv2  30906  friendshipgt3  31008  lpni  31091  nsnlplig  31092  nsnlpligALT  31093  n0lpligALT  31095  ipasslem5  31446  ipasslem11  31451  hhssnv  31875  shscli  31928  shsleji  31981  shsidmi  31995  spansncvi  32263  superpos  32965  chirredi  33005  mdsymlem6  33019  rnmposs  33318  1fldgenq  33934  ccfldextdgrr  34354  cnre2csqima  34593  dya2icobrsiga  34958  dya2iocnrect  34963  dya2iocucvr  34966  sxbrsigalem2  34968  afsval  35353  karddom  35889  kardsdom  35890  kardexen  35891  satfv0  36213  satfrnmapom  36225  satfv0fun  36226  satf00  36229  sat1el2xp  36234  fmla0xp  36238  fmla1  36242  msubco  36386  elaltxp  36836  altxpsspw  36838  funtransport  36892  funray  37001  funline  37003  ellines  37013  linethru  37014  icoreresf  38384  icoreclin  38389  relowlssretop  38395  relowlpssretop  38396  itg2addnc  38701  isline  40905  sn-it0e0  43576  sn-mullid  43596  sn-0tie0  43624  sn-mul02  43625  mzpcompact2lem  43871  sprvalpw  48670  sprvalpwn0  48673  prsprel  48677  prpair  48691  prprvalpw  48705  reuopreuprim  48716  nnsum3primesgbe  48998  nnsum4primesodd  49002  nnsum4primesoddALTV  49003  tgblthelfgott  49021  grtrif1o  49148  grtrissvtx  49150  gpgvtxel2  49254  pgn4cyclex  49332  nnpw2pb  49807  2arymaptf1  49873