Theorem rexlimivv 3204

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

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

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 3087

This theorem is used by:  r19.29vva  3222  2reu5  3716  2reu4  4480  opelxp  5691  elinxp  6012  reuop  6291  opiota  8056  f1o2ndf1  8119  poseq  8156  soseq  8157  tfrlem5  8368  xpdom2  9070  unxpdomlem3  9228  elfiun  9400  ttrcltr  9695  xpnum  9956  kmlem9  10161  nqereu  10938  distrlem5pr  11036  mulrid  11230  1re  11232  mul02  11412  cnegex  11415  recex  11870  creur  12236  creui  12237  cju  12238  elz2  12633  zaddcl  12658  qre  13002  qaddcl  13015  qnegcl  13016  qmulcl  13017  qreccl  13019  elpqb  13026  hash2prd  14540  elss2prb  14553  fundmge2nop0  14567  s3rex  15021  wrdl3s3  15035  replim  15203  prodmo  16023  odd2np1  16431  opoe  16453  omoe  16454  opeo  16455  omeo  16456  qredeu  16748  pythagtriplem1  16908  pcz  16973  4sqlem1  17040  4sqlem2  17041  4sqlem4  17044  mul4sq  17046  pmtr3ncom  19602  efgmnvl  19841  efgrelexlema  19876  ring1ne0  20441  pzriprnglem8  21701  txuni2  23791  tx2ndc  23877  blssioo  25021  tgioo  25022  ioorf  25801  ioorinv  25804  ioorcl  25805  dyaddisj  25824  mbfid  25863  elply  26420  vmacl  27354  efvmacl  27356  vmalelog  27441  2sqlem2  27654  mul2sq  27655  2sqlem7  27660  2sqnn0  27674  2sqreultblem  27684  pntibnd  27829  ostth  27875  cutsf  28057  zaddscl  28659  zmulscld  28662  elzn0s  28663  eln0zs  28665  zseo  28687  elz12s  28737  z12no  28741  z12addscl  28742  z12shalf  28745  z12zsodd  28747  z12bdaylem  28749  bdayfinlem  28751  remulscllem1  28765  legval  28926  upgredgpr  29599  nbgr2vtx1edg  29810  cusgredg  29884  usgredgsscusgredg  29919  wwlksnwwlksnon  30383  n4cyclfrgr  30771  vdgn1frgrv2  30776  friendshipgt3  30878  lpni  30961  nsnlplig  30962  nsnlpligALT  30963  n0lpligALT  30965  ipasslem5  31316  ipasslem11  31321  hhssnv  31745  shscli  31798  shsleji  31851  shsidmi  31865  spansncvi  32133  superpos  32835  chirredi  32875  mdsymlem6  32889  rnmposs  33146  1fldgenq  33763  ccfldextdgrr  34182  cnre2csqima  34421  dya2icobrsiga  34787  dya2iocnrect  34792  dya2iocucvr  34795  sxbrsigalem2  34797  afsval  35182  karddom  35687  kardsdom  35688  kardexen  35689  satfv0  35937  satfrnmapom  35949  satfv0fun  35950  satf00  35953  sat1el2xp  35958  fmla0xp  35962  fmla1  35966  msubco  36110  elaltxp  36555  altxpsspw  36557  funtransport  36611  funray  36720  funline  36722  ellines  36732  linethru  36733  icoreresf  38106  icoreclin  38111  relowlssretop  38117  relowlpssretop  38118  itg2addnc  38423  isline  40612  sn-it0e0  43291  sn-mullid  43311  sn-0tie0  43339  sn-mul02  43340  mzpcompact2lem  43596  sprvalpw  48380  sprvalpwn0  48383  prsprel  48387  prpair  48401  prprvalpw  48415  reuopreuprim  48426  nnsum3primesgbe  48708  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  tgblthelfgott  48731  grtrif1o  48858  grtrissvtx  48860  gpgvtxel2  48964  pgn4cyclex  49042  nnpw2pb  49517  2arymaptf1  49583