Theorem rexlimivv 3198

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3069

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-rex 3070

This theorem is referenced by:  r19.29vva  3212  2reu5  3755  2reu4  4527  opelxp  5713  elinxp  6020  reuop  6293  opiota  8048  f1o2ndf1  8111  poseq  8147  soseq  8148  tfrlem5  8383  xpdom2  9070  1sdomOLD  9252  unxpdomlem3  9255  unfiOLD  9316  elfiun  9428  ttrcltr  9714  xpnum  9949  kmlem9  10156  nqereu  10927  distrlem5pr  11025  mulrid  11217  1re  11219  mul02  11397  cnegex  11400  recex  11851  creur  12211  creui  12212  cju  12213  elz2  12581  zaddcl  12607  qre  12942  qaddcl  12954  qnegcl  12955  qmulcl  12956  qreccl  12958  elpqb  12965  hash2prd  14441  elss2prb  14453  fundmge2nop0  14458  wrdl3s3  14918  replim  15068  prodmo  15885  odd2np1  16289  opoe  16311  omoe  16312  opeo  16313  omeo  16314  qredeu  16600  pythagtriplem1  16754  pcz  16819  4sqlem1  16886  4sqlem2  16887  4sqlem4  16890  mul4sq  16892  pmtr3ncom  19385  efgmnvl  19624  efgrelexlema  19659  ring1ne0  20188  pzriprnglem8  21258  txuni2  23290  tx2ndc  23376  blssioo  24532  tgioo  24533  ioorf  25323  ioorinv  25326  ioorcl  25327  dyaddisj  25346  mbfid  25385  elply  25942  vmacl  26855  efvmacl  26857  vmalelog  26941  2sqlem2  27154  mul2sq  27155  2sqlem7  27160  2sqnn0  27174  2sqreultblem  27184  pntibnd  27329  ostth  27375  scutf  27547  legval  28099  upgredgpr  28666  nbgr2vtx1edg  28871  cusgredg  28945  usgredgsscusgredg  28980  wwlksnwwlksnon  29433  n4cyclfrgr  29808  vdgn1frgrv2  29813  friendshipgt3  29915  lpni  29997  nsnlplig  29998  nsnlpligALT  29999  n0lpligALT  30001  ipasslem5  30352  ipasslem11  30357  hhssnv  30781  shscli  30834  shsleji  30887  shsidmi  30901  spansncvi  31169  superpos  31871  chirredi  31911  mdsymlem6  31925  rnmposs  32163  1fldgenq  32679  ccfldextdgrr  33032  cnre2csqima  33186  dya2icobrsiga  33570  dya2iocnrect  33575  dya2iocucvr  33578  sxbrsigalem2  33580  afsval  33978  satfv0  34644  satfrnmapom  34656  satfv0fun  34657  satf00  34660  sat1el2xp  34665  fmla0xp  34669  fmla1  34673  msubco  34817  elaltxp  35248  altxpsspw  35250  funtransport  35304  funray  35413  funline  35415  ellines  35425  linethru  35426  icoreresf  36537  icoreclin  36542  relowlssretop  36548  relowlpssretop  36549  itg2addnc  36846  isline  38914  sn-it0e0  41591  sn-mullid  41611  sn-0tie0  41615  sn-mul02  41616  mzpcompact2lem  41792  sprvalpw  46448  sprvalpwn0  46451  prsprel  46455  prpair  46469  prprvalpw  46483  reuopreuprim  46494  nnsum3primesgbe  46760  nnsum4primesodd  46764  nnsum4primesoddALTV  46765  tgblthelfgott  46783  nnpw2pb  47362  2arymaptf1  47428