Theorem rexlimdva 2648

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)

Hypothesis

Ref	Expression
rexlimdva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
rexlimdva	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdva

Step	Hyp	Ref	Expression
1		rexlimdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 115	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 2647	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∃wrex 2509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  rexlimdvaa  2649  rexlimivv  2654  rexlimdvv  2655  ralxfrd  4550  rexxfrd  4551  fvelimab  5683  foco2  5870  elunirn  5883  f1elima  5890  mpoexw  6349  tfrlem5  6450  tfrlemibacc  6462  tfrlemibfn  6464  tfr1onlembacc  6478  tfr1onlembfn  6480  tfrcllembacc  6491  tfrcllembfn  6493  frecabcl  6535  nnaordex  6664  nnawordex  6665  ectocld  6738  phpm  7015  dif1enen  7030  fin0  7035  fin0or  7036  fimax2gtri  7051  fidcenum  7111  suplub2ti  7156  supisoex  7164  enomnilem  7293  finomni  7295  enmkvlem  7316  exmidfodomrlemeldju  7365  exmidfodomrlemreseldju  7366  ltexnqq  7583  ltbtwnnqq  7590  prarloclem4  7673  prarloc2  7679  genprndl  7696  genprndu  7697  prmuloc2  7742  1idprl  7765  1idpru  7766  cauappcvgprlemdisj  7826  cauappcvgprlemladdru  7831  cauappcvgprlemladdrl  7832  caucvgprlemladdrl  7853  recexgt0sr  7948  map2psrprg  7980  suplocsrlem  7983  nntopi  8069  cnegexlem1  8309  cnegexlem2  8310  renegcl  8395  aptap  8785  supinfneg  9778  infsupneg  9779  qmulz  9806  elpq  9832  icc0r  10110  exbtwnzlemstep  10454  rebtwn2zlemstep  10459  ioo0  10466  ico0  10468  ioc0  10469  modqmuladd  10575  addmodlteq  10607  frec2uzrand  10614  frecuzrdgtcl  10621  frecuzrdgfunlem  10628  hashunlem  11013  reuccatpfxs1lem  11264  shftlem  11313  caucvgre  11478  resqrexlemgt0  11517  rexico  11718  negfi  11725  climuni  11790  climshftlemg  11799  climcn1  11805  serf0  11849  summodclem2  11879  zsumdc  11881  fsum2dlemstep  11931  mertenslem2  12033  ntrivcvgap  12045  zproddc  12076  fprod2dlemstep  12119  dvds1lem  12299  odd2np1lem  12369  odd2np1  12370  sqoddm1div8z  12383  ltoddhalfle  12390  halfleoddlt  12391  m1expo  12397  divalglemeunn  12418  divalglemex  12419  divalglemeuneg  12420  flodddiv4  12433  bezoutlemaz  12510  bezoutlembz  12511  dvdssqim  12531  ncoprmgcdne1b  12597  coprmdvds2  12601  divgcdcoprm0  12609  cncongr1  12611  cncongr2  12612  dvdsnprmd  12633  rpexp  12661  pythagtriplem1  12774  pc2dvds  12839  difsqpwdvds  12847  oddprmdvds  12863  prmpwdvds  12864  4sqlem11  12910  imasmnd2  13471  dfgrp3mlem  13617  imasgrp2  13633  issubg4m  13716  imasabl  13859  ringinvnzdiv  13999  imasring  14013  dvdsrcl2  14048  dvdsrmul1  14051  isnzr2  14133  lss1d  14332  lssats2  14363  lspsn  14365  dvdsrzring  14552  znunit  14608  znrrg  14609  tgcl  14723  innei  14822  cnptoprest  14898  lmss  14905  lmtopcnp  14909  txlm  14938  blssps  15086  blss  15087  blssexps  15088  blssex  15089  mopni3  15143  metrest  15165  metcnp3  15170  mulc1cncf  15248  cncfco  15250  elply2  15394  gausslemma2dlem1a  15722  lgsquadlem1  15741  2lgsoddprmlem2  15770  subctctexmid  16297