Theorem rexlimivv 3209

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

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

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 3092

This theorem is used by:  r19.29vva  3227  2reu5  3723  2reu4  4487  opelxp  5699  elinxp  6020  reuop  6298  opiota  8062  f1o2ndf1  8123  poseq  8160  soseq  8161  tfrlem5  8372  xpdom2  9067  unxpdomlem3  9225  elfiun  9397  ttrcltr  9692  xpnum  9953  kmlem9  10158  nqereu  10929  distrlem5pr  11027  mulrid  11221  1re  11223  mul02  11403  cnegex  11406  recex  11861  creur  12227  creui  12228  cju  12229  elz2  12624  zaddcl  12649  qre  12993  qaddcl  13005  qnegcl  13006  qmulcl  13007  qreccl  13009  elpqb  13016  hash2prd  14530  elss2prb  14543  fundmge2nop0  14557  wrdl3s3  15023  replim  15191  prodmo  16013  odd2np1  16421  opoe  16443  omoe  16444  opeo  16445  omeo  16446  qredeu  16738  pythagtriplem1  16898  pcz  16963  4sqlem1  17030  4sqlem2  17031  4sqlem4  17034  mul4sq  17036  pmtr3ncom  19589  efgmnvl  19828  efgrelexlema  19863  ring1ne0  20428  pzriprnglem8  21688  txuni2  23773  tx2ndc  23859  blssioo  25003  tgioo  25004  ioorf  25783  ioorinv  25786  ioorcl  25787  dyaddisj  25806  mbfid  25845  elply  26403  vmacl  27333  efvmacl  27335  vmalelog  27420  2sqlem2  27633  mul2sq  27634  2sqlem7  27639  2sqnn0  27653  2sqreultblem  27663  pntibnd  27808  ostth  27854  cutsf  28036  zaddscl  28638  zmulscld  28641  elzn0s  28642  eln0zs  28644  zseo  28666  elz12s  28716  z12no  28720  z12addscl  28721  z12shalf  28724  z12zsodd  28726  z12bdaylem  28728  bdayfinlem  28730  remulscllem1  28744  legval  28904  upgredgpr  29547  nbgr2vtx1edg  29758  cusgredg  29832  usgredgsscusgredg  29867  wwlksnwwlksnon  30331  n4cyclfrgr  30713  vdgn1frgrv2  30718  friendshipgt3  30820  lpni  30903  nsnlplig  30904  nsnlpligALT  30905  n0lpligALT  30907  ipasslem5  31258  ipasslem11  31263  hhssnv  31687  shscli  31740  shsleji  31793  shsidmi  31807  spansncvi  32075  superpos  32777  chirredi  32817  mdsymlem6  32831  rnmposs  33089  1fldgenq  33707  ccfldextdgrr  34126  cnre2csqima  34365  dya2icobrsiga  34731  dya2iocnrect  34736  dya2iocucvr  34739  sxbrsigalem2  34741  afsval  35126  karddom  35631  kardsdom  35632  kardexen  35633  satfv0  35887  satfrnmapom  35899  satfv0fun  35900  satf00  35903  sat1el2xp  35908  fmla0xp  35912  fmla1  35916  msubco  36060  elaltxp  36504  altxpsspw  36506  funtransport  36560  funray  36669  funline  36671  ellines  36681  linethru  36682  icoreresf  38055  icoreclin  38060  relowlssretop  38066  relowlpssretop  38067  itg2addnc  38382  isline  40571  sn-it0e0  43235  sn-mullid  43255  sn-0tie0  43283  sn-mul02  43284  mzpcompact2lem  43540  sprvalpw  48287  sprvalpwn0  48290  prsprel  48294  prpair  48308  prprvalpw  48322  reuopreuprim  48333  nnsum3primesgbe  48615  nnsum4primesodd  48619  nnsum4primesoddALTV  48620  tgblthelfgott  48638  grtrif1o  48765  grtrissvtx  48767  gpgvtxel2  48871  pgn4cyclex  48949  nnpw2pb  49424  2arymaptf1  49490