Theorem rexlimivv 3180

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  r19.29vva  3198  2reu5  3705  2reu4  4465  opelxp  5661  elinxp  5979  reuop  6252  opiota  8006  f1o2ndf1  8066  poseq  8102  soseq  8103  tfrlem5  8313  xpdom2  9004  unxpdomlem3  9162  elfiun  9337  ttrcltr  9631  xpnum  9869  kmlem9  10075  nqereu  10846  distrlem5pr  10944  mulrid  11136  1re  11138  mul02  11318  cnegex  11321  recex  11776  creur  12147  creui  12148  cju  12149  elz2  12536  zaddcl  12561  qre  12897  qaddcl  12909  qnegcl  12910  qmulcl  12911  qreccl  12913  elpqb  12920  hash2prd  14431  elss2prb  14444  fundmge2nop0  14458  wrdl3s3  14918  replim  15072  prodmo  15895  odd2np1  16304  opoe  16326  omoe  16327  opeo  16328  omeo  16329  qredeu  16621  pythagtriplem1  16781  pcz  16846  4sqlem1  16913  4sqlem2  16914  4sqlem4  16917  mul4sq  16919  pmtr3ncom  19444  efgmnvl  19683  efgrelexlema  19718  ring1ne0  20274  pzriprnglem8  21481  txuni2  23543  tx2ndc  23629  blssioo  24773  tgioo  24774  ioorf  25553  ioorinv  25556  ioorcl  25557  dyaddisj  25576  mbfid  25615  elply  26173  vmacl  27098  efvmacl  27100  vmalelog  27185  2sqlem2  27398  mul2sq  27399  2sqlem7  27404  2sqnn0  27418  2sqreultblem  27428  pntibnd  27573  ostth  27619  cutsf  27801  zaddscl  28403  zmulscld  28406  elzn0s  28407  eln0zs  28409  zseo  28431  elz12s  28481  z12no  28485  z12addscl  28486  z12shalf  28489  z12zsodd  28491  z12bdaylem  28493  bdayfinlem  28495  remulscllem1  28509  legval  28669  upgredgpr  29228  nbgr2vtx1edg  29436  cusgredg  29510  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  32764  1fldgenq  33401  ccfldextdgrr  33835  cnre2csqima  34074  dya2icobrsiga  34439  dya2iocnrect  34444  dya2iocucvr  34447  sxbrsigalem2  34449  afsval  34834  satfv0  35559  satfrnmapom  35571  satfv0fun  35572  satf00  35575  sat1el2xp  35580  fmla0xp  35584  fmla1  35588  msubco  35732  elaltxp  36176  altxpsspw  36178  funtransport  36232  funray  36341  funline  36343  ellines  36353  linethru  36354  icoreresf  37685  icoreclin  37690  relowlssretop  37696  relowlpssretop  37697  itg2addnc  38012  isline  40202  sn-it0e0  42865  sn-mullid  42885  sn-0tie0  42913  sn-mul02  42914  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