Theorem rexlimdva 3169

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 418	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3167	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

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

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 3093

This theorem is used by:  rexlimdvaa  3170  rexlimivv  3210  rexlimdvv  3224  rspceb2dv  3588  ssexnelpss  4074  ralxfrd2  5388  iunopeqop  5509  iunopeqopOLD  5510  elsnxp  6299  foco2  7111  elunirn  7256  f1elima  7268  mptcnfimad  7992  releldmdifi  8051  mpoexw  8084  xpord3pred  8157  sexp3  8158  tfrlem9a  8382  seqomlem2  8447  oawordexr  8550  odi  8573  oelimcl  8595  nnawordex  8632  nnaordex  8633  oaabs  8643  oaabs2  8644  omabs  8646  eldifsucnn  8659  coflton  8666  cofon1  8667  cofon2  8668  cofonr  8669  naddunif  8689  ectocld  8789  onfin  9209  dif1ennnALT  9247  isfinite2  9268  isfiniteg  9270  fofinf1o  9299  elfiun  9400  suplub2  9431  supisoex  9445  ordtypelem9  9498  ordtypelem10  9499  brwdom2  9545  brwdom3  9554  ttrcltr  9695  rankr1ai  9780  fodomfi2  10063  infpwfien  10065  dfac12r  10149  ackbij1  10239  cff1  10260  fin23lem21  10341  isf32lem2  10356  fin1a2lem11  10412  fin1a2lem13  10414  ficard  10567  gchina  10702  eltsk2g  10754  tskr1om2  10771  rankcf  10780  inatsk  10781  tskuni  10786  nqereu  10932  ltexnq  10978  1idpr  11032  suplem1pr  11055  supsrlem  11114  axpre-sup  11172  1re  11226  0re  11228  0cnALT  11463  supaddc  12200  supadd  12201  supmul1  12202  supmul  12205  suprzcl2  12980  qmulz  12993  elpq  13017  qbtwnre  13243  ioo0  13415  ico0  13436  ioc0  13437  icc0  13438  addmodlteq  14002  fsequb  14031  hashdom  14435  ccats1alpha  14679  reuccatpfxs1lem  14807  shftlem  15131  rexuzre  15430  rexico  15431  caubnd  15436  limsupbnd1  15559  limsupbnd2  15560  rlim2lt  15574  rlim3  15575  lo1bdd2  15601  lo1bddrp  15602  o1lo1  15614  climuni  15629  climshftlem  15651  o1co  15663  rlimcn1  15665  climcn1  15669  o1rlimmul  15696  lo1le  15729  rlimno1  15731  isercoll  15745  caurcvg2  15755  serf0  15758  summolem2  15793  zsum  15795  fsum2dlem  15847  geomulcvg  15956  mertenslem2  15965  ntrivcvg  15977  zprod  16017  fprod2dlem  16060  dvds1lem  16350  dvdsexp2im  16410  odd2np1lem  16423  sqoddm1div8z  16437  ltoddhalfle  16444  halfleoddlt  16445  flodddiv4  16498  dvdssqim  16637  dvdsexpim  16638  coprmdvds2  16737  divgcdcoprm0  16748  cncongr1  16750  cncongr2  16751  isprm5  16791  rpexp  16806  pythagtriplem1  16901  iserodd  16920  pc2dvds  16964  difsqpwdvds  16972  oddprmdvds  16988  prmpwdvds  16989  4sqlem11  17040  vdwapun  17059  vdwlem2  17067  vdwlem6  17071  vdwlem8  17073  vdwlem10  17075  vdwnnlem1  17080  vdwnnlem3  17082  0ram  17105  ramub1lem2  17112  ramcl  17114  cshwsiun  17184  cshwrepswhash1  17187  firest  17510  imasvscafn  17616  imasmnd2  18863  dfgrp3lem  19135  imasgrp2  19152  issubg4  19243  cycsubm  19304  gaorber  19409  orbsta  19414  pmtr3ncom  19576  psgnran  19616  odmulg  19657  odbezout  19659  gexdvdsi  19684  sylow1lem3  19701  odcau  19705  sylow2alem1  19718  sylow3lem6  19733  lsmelvalm  19752  efgrelexlemb  19851  efgredeu  19853  imasabl  19977  cyggeninv  19984  cygctb  19993  cyggexb  20000  dprdssv  20119  dprddisj2  20142  ablfacrplem  20168  pgpfac1lem2  20178  pgpfac1lem5  20182  ringinvnzdiv  20417  imasring  20445  dvdsrcl2  20481  dvdsrmul1  20484  lss1d  21121  lssats2  21158  lspsn  21160  lmhmima  21205  rspsn0  21409  ring2idlqusb  21487  rngqiprngfulem2  21489  lpiss  21534  dvdsrzring  21648  pzriprnglem5  21672  pzriprnglem8  21675  pzriprnglem10  21677  pzriprnglem11  21678  znunit  21750  znrrg  21752  cygznlem3  21756  frgpcyg  21760  lindfrn  22008  mplcoe5lem  22227  mpfind  22303  gsummoncoe1  22505  mpfpf1  22548  pf1mpf  22549  mat1dimelbas  22665  scmatdmat  22709  scmataddcl  22710  scmatsubcl  22711  scmatmulcl  22712  cpmatacl  22910  chpscmat  23036  tgcl  23163  clsval2  23244  innei  23319  restcld  23366  restcldr  23368  ordtrest2lem  23397  cnprest  23483  lmss  23492  lmcls  23496  lmcnp  23498  isreg2  23571  cmpcovf  23585  cncmp  23586  cmpsub  23594  1stcrest  23647  2ndcrest  23648  1stccnp  23656  restnlly  23676  cldllycmp  23689  locfincmp  23720  txcnpi  23802  pthaus  23832  txtube  23834  txcmplem1  23835  txcmplem2  23836  txlm  23842  xkohaus  23847  xkococnlem  23853  xkococn  23854  kqfvima  23924  kqreglem1  23935  isfild  24052  filuni  24079  isufil2  24102  uffix  24115  rnelfm  24147  fmfnfmlem2  24149  fmfnfmlem4  24151  fmfnfm  24152  fmco  24155  fclsopn  24208  ufilcmp  24226  cnpfcf  24235  alexsublem  24238  alexsubALT  24245  cldsubg  24305  ghmcnp  24309  qustgpopn  24314  tsmsgsum  24333  tsmsres  24338  tsmsxplem1  24347  tsmsxp  24349  isucn2  24472  ucnprima  24475  imasdsf1olem  24567  blssps  24618  blss  24619  blssexps  24620  blssex  24621  mopni3  24688  blcld  24699  metrest  24718  metcnp3  24734  reperflem  25013  icccmplem3  25019  xrge0tsms  25029  mulc1cncf  25101  cncfco  25103  cnheibor  25151  bndth  25154  lebnumlem3  25159  xlebnum  25161  lebnumii  25162  nmhmcn  25316  cfil3i  25465  cmetcaulem  25484  cfilres  25492  bcthlem4  25523  ivthlem2  25648  ivthlem3  25649  ivthicc  25654  cniccbdd  25657  ovolunlem1  25693  ovoliunlem2  25699  ovolshftlem2  25706  ovolicc2  25718  iunmbl2  25753  dyadmax  25794  opnmbllem  25797  subopnmbl  25800  volivth  25803  ismbf3d  25850  mbfimaopn2  25853  mbfaddlem  25856  i1fmullem  25890  mbfi1fseqlem4  25914  bddiblnc  26038  ellimc3  26075  dvlip  26189  dvlip2  26191  c1liplem1  26192  dvgt0lem1  26198  dvivthlem2  26205  dvne0  26207  lhop1lem  26209  lhop2  26211  lhop  26212  tdeglem4  26254  mdegnn0cl  26265  ply1divex  26331  dvdsq1p  26357  ig1peu  26369  elply2  26390  plypf1  26406  plydivex  26495  aalioulem3  26534  aalioulem5  26536  aaliou  26538  ulmshftlem  26589  ulmcau  26595  ulmss  26597  ulmbdd  26598  ulmcn  26599  radcnvlt1  26618  eflogeq  26804  efopn  26860  cxpeq  26959  angpieqvd  27033  xrlimcnp  27170  cxploglim  27179  ftalem2  27275  ftalem7  27280  isppw2  27316  dchrptlem1  27465  dchrptlem3  27467  dchrsum2  27469  lgsdchrval  27555  lgsdchr  27556  gausslemma2dlem1a  27566  lgsquadlem1  27581  2lgsoddprmlem2  27610  dchrisumlem3  27692  dchrisum0fno1  27712  pntlem3  27810  pntleml  27812  ostth3  27839  nosupno  27904  nosupbday  27906  noinfbday  27921  cutsun12  28020  oldssmade  28097  addsproplem2  28200  addsuniflem  28231  addbdaylem  28247  negsid  28271  negsunif  28285  negleft  28288  negright  28289  precsexlem6  28442  precsexlem7  28443  precsexlem11  28447  bdayons  28506  onaddscl  28507  om2noseqlt  28529  noseqrdgfn  28536  n0fincut  28585  bdayn0sf1o  28600  dfnns2  28602  bdaypw2n0bndlem  28693  bdayfinbndlem1  28697  z12negscl  28708  z12zsodd  28712  z12bdaylem  28714  bdayfinlem  28716  recut  28724  elreno2  28725  brcgr  29287  brbtwn2  29292  axbtwnid  29326  axcontlem7  29357  usgrnloopALT  29590  uhgrspansubgrlem  29677  nbuhgr  29730  nbupgr  29731  wwlksnextprop  30298  elwspths2on  30348  elwspths2onw  30349  erclwwlktr  30410  clwwlknscsh  30450  erclwwlkntr  30459  hashecclwwlkn1  30465  umgrhashecclwwlk  30466  3cyclfrgrrn1  30673  frgrregorufr  30713  frgr2wwlk1  30717  ubthlem1  31259  ubthlem3  31261  htthlem  31306  omlsii  31792  spansncol  31957  nmopun  32403  nmcexi  32415  riesz1  32454  elpjrn  32579  cvcon3  32673  chcv1  32744  atcvatlem  32774  chirredi  32783  br8d  32990  xrge0tsmsd  33424  ordtrest2NEWlem  34343  lmxrge0  34373  esumfsup  34491  esumpcvgval  34499  measdivcstALTV  34647  eulerpartlemgh  34800  dstfrvunirn  34897  afsval  35093  onvf1odlem4  35614  erdszelem8  35711  erdszelem11  35714  erdsze2lem2  35717  connpconn  35748  sconnpi1  35752  cvmsss2  35787  cvmfolem  35792  cvmliftmolem2  35795  cvmliftlem15  35811  cvmlift2lem1  35815  cvmlift3lem4  35835  cvmlift3lem5  35836  satfdmlem  35881  fmla1  35900  gonarlem  35907  gonar  35908  goalrlem  35909  goalr  35910  fmla0disjsuc  35911  fmlasucdisj  35912  satffunlem1lem1  35915  satffunlem1lem2  35916  satffunlem2lem1  35917  mrsub0  36029  mrsubcn  36032  msubrn  36042  msubvrs  36073  br8  36269  br6  36270  br4  36271  cgrtriv  36515  btwntriv2  36525  btwncomim  36526  btwnswapid  36530  btwnintr  36532  btwnexch3  36533  btwnouttr2  36535  ifscgr  36557  cgrxfr  36568  btwnxfr  36569  btwnconn3  36616  segcon2  36618  brsegle  36621  seglecgr12im  36623  broutsideof3  36639  linethru  36666  elhf2  36688  nmulprop  36703  opnregcld  36882  cldregopn  36883  neibastop2lem  36912  tr0elw  37036  tr0el  37037  matunitlindflem1  38308  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem24  38336  poimirlem29  38341  heicant  38347  opnmbllem0  38348  ismblfin  38353  itg2addnclem  38363  itg2addnclem3  38365  itg2gt0cn  38367  ftc1anclem5  38389  ftc2nc  38394  filbcmb  38432  fdc  38437  incsequz  38440  caushft  38453  istotbnd3  38463  equivbnd  38482  cntotbnd  38488  heibor1lem  38501  heibor1  38502  bfplem2  38515  divrngidl  38720  prnc  38759  lshpdisj  39802  cvrcon3b  40092  atnle  40132  hlhgt2  40204  hl0lt1N  40205  hl2at  40220  cvrexchlem  40234  cvratlem  40236  lvolnlelpln  40400  2lplnj  40435  ispsubcl2N  40762  lautcvr  40907  dva1dim  41800  dib1dim  41980  dib1dim2  41983  diclspsn  42009  dih1dimatlem  42144  dihlatat  42152  dihatexv  42153  dihatexv2  42154  lcfrlem9  42365  lcfrlem16  42373  mapdrvallem2  42460  mapd1o  42463  aks6d1c2  42938  elre0re  43063  prjspner1  43399  dffltz  43407  rexlimdv3d  43455  elrfi  43466  isnacs3  43482  eldiophb  43529  eldiophss  43546  diophren  43581  rencldnfilem  43588  pell1234qrdich  43629  pellfundex  43654  lsmfgcl  43842  kercvrlsm  43851  lmhmfgima  43852  lpirlnr  43885  hbtlem2  43892  hbtlem4  43894  hbtlem6  43897  rngunsnply  43937  onexoegt  44012  oaabsb  44062  cantnfresb  44092  omabs2  44100  tfsconcatrev  44116  restuni3  45877  limsupubuz  46468  stoweidlem57  46812  fourierdlem48  46909  fourierdlem49  46910  sge0le  47162  fsetsniunop  47827  cfsetsnfsetfo  47838  fcoresf1  47847  euoreqb  47887  modlt0b  48147  nndivides2  48162  imasetpreimafvbijlemf1  48194  imasetpreimafvbijlemfo  48195  iccpartrn  48220  iccpartiun  48224  iccpartnel  48228  paireqne  48301  reupr  48312  odz2prm2pw  48356  fmtnofac2lem  48361  prmdvdsfmtnof1lem2  48378  2pwp1prm  48382  mod42tp1mod8  48395  lighneallem3  48400  lighneallem4  48403  nprmdvdsfacm1  48417  ppivalnnprm  48418  ppivalnnnprmge6  48419  requad01  48427  requad2  48429  fppr2odd  48537  gbowpos  48565  gbowgt5  48568  gboge9  48570  nnsum4primesodd  48602  nnsum4primesoddALTV  48603  isubgredg  48672  grimcnv  48694  uhgrimedgi  48696  isuspgrim0  48700  isuspgrimlem  48701  gricushgr  48723  clnbgrgrimlem  48739  clnbgrgrim  48740  grimedg  48741  grtrissvtx  48750  stgrusgra  48765  isubgr3stgrlem7  48778  gpgiedgdmellem  48852  gpgusgralem  48862  gpgvtxedg0  48869  gpgvtxedg1  48870  copisnmnd  48975  lidldomn1  49037  affinecomb1  49523  eenglngeehlnmlem2  49559  rrx2vlinest  49562  itsclquadb  49597  aacllem  50662