Theorem rexlimivv 3179

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  r19.29vva  3197  2reu5  3729  2reu4  4486  opelxp  5674  elinxp  5990  reuop  6266  opiota  8038  f1o2ndf1  8101  poseq  8137  soseq  8138  tfrlem5  8348  xpdom2  9036  1sdomOLD  9196  unxpdomlem3  9199  elfiun  9381  ttrcltr  9669  xpnum  9904  kmlem9  10112  nqereu  10882  distrlem5pr  10980  mulrid  11172  1re  11174  mul02  11352  cnegex  11355  recex  11810  creur  12180  creui  12181  cju  12182  elz2  12547  zaddcl  12573  qre  12912  qaddcl  12924  qnegcl  12925  qmulcl  12926  qreccl  12928  elpqb  12935  hash2prd  14440  elss2prb  14453  fundmge2nop0  14467  wrdl3s3  14928  replim  15082  prodmo  15902  odd2np1  16311  opoe  16333  omoe  16334  opeo  16335  omeo  16336  qredeu  16628  pythagtriplem1  16787  pcz  16852  4sqlem1  16919  4sqlem2  16920  4sqlem4  16923  mul4sq  16925  pmtr3ncom  19405  efgmnvl  19644  efgrelexlema  19679  ring1ne0  20208  pzriprnglem8  21398  txuni2  23452  tx2ndc  23538  blssioo  24683  tgioo  24684  ioorf  25474  ioorinv  25477  ioorcl  25478  dyaddisj  25497  mbfid  25536  elply  26100  vmacl  27028  efvmacl  27030  vmalelog  27116  2sqlem2  27329  mul2sq  27330  2sqlem7  27335  2sqnn0  27349  2sqreultblem  27359  pntibnd  27504  ostth  27550  scutf  27724  zaddscl  28282  zmulscld  28285  elzn0s  28286  eln0zs  28288  zseo  28308  elzs12  28337  zs12bday  28343  remulscllem1  28351  legval  28511  upgredgpr  29069  nbgr2vtx1edg  29277  cusgredg  29351  usgredgsscusgredg  29387  wwlksnwwlksnon  29845  n4cyclfrgr  30220  vdgn1frgrv2  30225  friendshipgt3  30327  lpni  30409  nsnlplig  30410  nsnlpligALT  30411  n0lpligALT  30413  ipasslem5  30764  ipasslem11  30769  hhssnv  31193  shscli  31246  shsleji  31299  shsidmi  31313  spansncvi  31581  superpos  32283  chirredi  32323  mdsymlem6  32337  rnmposs  32598  1fldgenq  33272  ccfldextdgrr  33667  cnre2csqima  33901  dya2icobrsiga  34267  dya2iocnrect  34272  dya2iocucvr  34275  sxbrsigalem2  34277  afsval  34662  satfv0  35345  satfrnmapom  35357  satfv0fun  35358  satf00  35361  sat1el2xp  35366  fmla0xp  35370  fmla1  35374  msubco  35518  elaltxp  35963  altxpsspw  35965  funtransport  36019  funray  36128  funline  36130  ellines  36140  linethru  36141  icoreresf  37340  icoreclin  37345  relowlssretop  37351  relowlpssretop  37352  itg2addnc  37668  isline  39733  sn-it0e0  42404  sn-mullid  42424  sn-0tie0  42439  sn-mul02  42440  mzpcompact2lem  42739  sprvalpw  47481  sprvalpwn0  47484  prsprel  47488  prpair  47502  prprvalpw  47516  reuopreuprim  47527  nnsum3primesgbe  47793  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  tgblthelfgott  47816  grtrif1o  47941  grtrissvtx  47943  gpgvtxel2  48039  pgn4cyclex  48116  nnpw2pb  48576  2arymaptf1  48642