Theorem rexlimivv 3220

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  r19.29vva  3263  2reu5  3688  2reu4  4454  opelxp  5616  elinxp  5918  reuop  6185  opiota  7872  f1o2ndf1  7934  tfrlem5  8182  xpdom2  8807  1sdom  8955  unxpdomlem3  8958  unfiOLD  9011  elfiun  9119  xpnum  9640  kmlem9  9845  nqereu  10616  distrlem5pr  10714  mulid1  10904  1re  10906  mul02  11083  cnegex  11086  recex  11537  creur  11897  creui  11898  cju  11899  elz2  12267  zaddcl  12290  qre  12622  qaddcl  12634  qnegcl  12635  qmulcl  12636  qreccl  12638  elpqb  12645  hash2prd  14117  elss2prb  14129  fundmge2nop0  14134  wrdl3s3  14605  replim  14755  prodmo  15574  odd2np1  15978  opoe  16000  omoe  16001  opeo  16002  omeo  16003  qredeu  16291  pythagtriplem1  16445  pcz  16510  4sqlem1  16577  4sqlem2  16578  4sqlem4  16581  mul4sq  16583  pmtr3ncom  18998  efgmnvl  19235  efgrelexlema  19270  ring1ne0  19745  txuni2  22624  tx2ndc  22710  blssioo  23864  tgioo  23865  ioorf  24642  ioorinv  24645  ioorcl  24646  dyaddisj  24665  mbfid  24704  elply  25261  vmacl  26172  efvmacl  26174  vmalelog  26258  2sqlem2  26471  mul2sq  26472  2sqlem7  26477  2sqnn0  26491  2sqreultblem  26501  pntibnd  26646  ostth  26692  legval  26849  upgredgpr  27415  nbgr2vtx1edg  27620  cusgredg  27694  usgredgsscusgredg  27729  wwlksnwwlksnon  28181  n4cyclfrgr  28556  vdgn1frgrv2  28561  friendshipgt3  28663  lpni  28743  nsnlplig  28744  nsnlpligALT  28745  n0lpligALT  28747  ipasslem5  29098  ipasslem11  29103  hhssnv  29527  shscli  29580  shsleji  29633  shsidmi  29647  spansncvi  29915  superpos  30617  chirredi  30657  mdsymlem6  30671  rnmposs  30913  ccfldextdgrr  31644  cnre2csqima  31763  dya2icobrsiga  32143  dya2iocnrect  32148  dya2iocucvr  32151  sxbrsigalem2  32153  afsval  32551  satfv0  33220  satfrnmapom  33232  satfv0fun  33233  satf00  33236  sat1el2xp  33241  fmla0xp  33245  fmla1  33249  msubco  33393  ttrcltr  33702  poxp3  33723  poseq  33729  soseq  33730  scutf  33933  elaltxp  34204  altxpsspw  34206  funtransport  34260  funray  34369  funline  34371  ellines  34381  linethru  34382  icoreresf  35450  icoreclin  35455  relowlssretop  35461  relowlpssretop  35462  itg2addnc  35758  isline  37680  sn-it0e0  40318  sn-mulid2  40338  sn-0tie0  40342  sn-mul02  40343  mzpcompact2lem  40489  sprvalpw  44820  sprvalpwn0  44823  prsprel  44827  prpair  44841  prprvalpw  44855  reuopreuprim  44866  nnsum3primesgbe  45132  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  tgblthelfgott  45155  nnpw2pb  45821  2arymaptf1  45887