Theorem rexlimivv 3181

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3064

This theorem is referenced by:  r19.29vva  3199  2reu5  3699  2reu4  4452  opelxp  5654  elinxp  5971  reuop  6244  opiota  8001  f1o2ndf1  8061  poseq  8098  soseq  8099  tfrlem5  8309  xpdom2  9000  unxpdomlem3  9158  elfiun  9333  ttrcltr  9628  xpnum  9866  kmlem9  10072  nqereu  10843  distrlem5pr  10941  mulrid  11133  1re  11135  mul02  11315  cnegex  11318  recex  11773  creur  12144  creui  12145  cju  12146  elz2  12533  zaddcl  12558  qre  12894  qaddcl  12906  qnegcl  12907  qmulcl  12908  qreccl  12910  elpqb  12917  hash2prd  14428  elss2prb  14441  fundmge2nop0  14455  wrdl3s3  14915  replim  15069  prodmo  15892  odd2np1  16301  opoe  16323  omoe  16324  opeo  16325  omeo  16326  qredeu  16618  pythagtriplem1  16778  pcz  16843  4sqlem1  16910  4sqlem2  16911  4sqlem4  16914  mul4sq  16916  pmtr3ncom  19441  efgmnvl  19680  efgrelexlema  19715  ring1ne0  20271  pzriprnglem8  21463  txuni2  23548  tx2ndc  23634  blssioo  24778  tgioo  24779  ioorf  25558  ioorinv  25561  ioorcl  25562  dyaddisj  25581  mbfid  25620  elply  26178  vmacl  27099  efvmacl  27101  vmalelog  27186  2sqlem2  27399  mul2sq  27400  2sqlem7  27405  2sqnn0  27419  2sqreultblem  27429  pntibnd  27574  ostth  27620  cutsf  27802  zaddscl  28404  zmulscld  28407  elzn0s  28408  eln0zs  28410  zseo  28432  elz12s  28482  z12no  28486  z12addscl  28487  z12shalf  28490  z12zsodd  28492  z12bdaylem  28494  bdayfinlem  28496  remulscllem1  28510  legval  28670  upgredgpr  29229  nbgr2vtx1edg  29437  cusgredg  29511  usgredgsscusgredg  29546  wwlksnwwlksnon  30001  n4cyclfrgr  30379  vdgn1frgrv2  30384  friendshipgt3  30486  lpni  30569  nsnlplig  30570  nsnlpligALT  30571  n0lpligALT  30573  ipasslem5  30924  ipasslem11  30929  hhssnv  31353  shscli  31406  shsleji  31459  shsidmi  31473  spansncvi  31741  superpos  32443  chirredi  32483  mdsymlem6  32497  rnmposs  32765  1fldgenq  33406  ccfldextdgrr  33856  cnre2csqima  34095  dya2icobrsiga  34460  dya2iocnrect  34465  dya2iocucvr  34468  sxbrsigalem2  34470  afsval  34855  satfv0  35586  satfrnmapom  35598  satfv0fun  35599  satf00  35602  sat1el2xp  35607  fmla0xp  35611  fmla1  35615  msubco  35759  elaltxp  36203  altxpsspw  36205  funtransport  36259  funray  36368  funline  36370  ellines  36380  linethru  36381  icoreresf  37714  icoreclin  37719  relowlssretop  37725  relowlpssretop  37726  itg2addnc  38041  isline  40231  sn-it0e0  42893  sn-mullid  42913  sn-0tie0  42941  sn-mul02  42942  mzpcompact2lem  43200  sprvalpw  47955  sprvalpwn0  47958  prsprel  47962  prpair  47976  prprvalpw  47990  reuopreuprim  48001  nnsum3primesgbe  48283  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  tgblthelfgott  48306  grtrif1o  48433  grtrissvtx  48435  gpgvtxel2  48539  pgn4cyclex  48617  nnpw2pb  49078  2arymaptf1  49144