Theorem rexlimdv 3211

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

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

Proof of Theorem rexlimdv

Step	Hyp	Ref	Expression
1		rexlimdv.1	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
2	1	com3l 89	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜓 → (𝜑 → 𝜒)))
3	2	rexlimiv 3208	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 → (𝜑 → 𝜒))
4	3	com12 32	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∈ 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:  rexlimdva  3212  rexlimdv3a  3214  rexlimdva2  3215  rexlimdvw  3218  rexlimdvv  3221  elpwunsn  4616  eldmrexrnb  6950  weniso  7205  ssorduni  7606  onint  7617  limuni3  7674  peano5  7714  funcnvuni  7752  funeldmdif  7862  frxp  7938  smoiun  8163  tfrlem9  8187  oaordex  8351  oalimcl  8353  oaass  8354  findcard2  8909  findcard3  8987  frfi  8989  unblem1  8996  ordiso2  9204  inf3lem3  9318  trpredrec  9415  r1sdom  9463  tz9.12lem3  9478  karden  9584  infxpenlem  9700  cardinfima  9784  iunfictbso  9801  dfac5  9815  cfcoflem  9959  fin23lem11  10004  fin23lem30  10029  fin1a2lem13  10099  axdc3lem2  10138  konigthlem  10255  fpwwe2lem11  10328  tskuni  10470  axgroth6  10515  nqereu  10616  genpnmax  10694  ltaddpr  10721  recexsrlem  10790  mulgt0sr  10792  axrrecex  10850  axpre-sup  10856  addid1  11085  addid2  11088  recex  11537  btwnz  12352  lbzbi  12605  qbtwnre  12862  caubnd  14998  divalglem9  16038  unbenlem  16537  firest  17060  imasmnd2  18337  imasgrp2  18605  pmtrfrn  18981  pgpfi  19125  sylow2blem3  19142  imasring  19773  lspsneq  20299  lspdisj  20302  elcls  22132  elcls3  22142  subbascn  22313  cmpsublem  22458  cmpsub  22459  nllyidm  22548  comppfsc  22591  ptpjopn  22671  fbfinnfr  22900  filin  22913  isfil2  22915  infil  22922  fgss2  22933  fgfil  22934  fgcl  22937  fgabs  22938  elfm2  23007  rnelfm  23012  fmfnfmlem2  23014  fmfnfmlem4  23016  fmco  23020  flffbas  23054  cnpflf2  23059  fclscf  23084  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  alexsubALT  23110  neibl  23563  met2ndc  23585  metcnp3  23602  icccmplem2  23892  xrge0tsms  23903  fgcfil  24340  volfiniun  24616  dyadmax  24667  dyadmbllem  24668  c1liplem1  25065  dgrlem  25295  axcontlem10  27244  usgredg2vtxeuALT  27492  ushgredgedg  27499  ushgredgedgloop  27501  uhgrspan1  27573  nbuhgr2vtx1edgblem  27621  erclwwlksym  28286  erclwwlknsym  28335  1pthon2v  28418  conngrv2edg  28460  lpni  28743  grpoidinvlem3  28769  grporcan  28781  omlsii  29666  spansncol  29831  spansnss  29834  spanunsni  29842  h1datomi  29844  nmopsetretALT  30126  branmfn  30368  chjatom  30620  cvbr4i  30630  atomli  30645  xrge0tsmsd  31219  umgr2cycllem  33002  umgr2cycl  33003  sat1el2xp  33241  fmlasuc  33248  satffunlem1lem2  33265  satffunlem2lem1  33266  satffunlem2lem2  33268  onelssex  33563  dfon2lem6  33670  colineardim1  34290  finminlem  34434  nn0prpwlem  34438  neibastop2lem  34476  neibastop2  34477  fgmin  34486  exrecfnlem  35477  heiborlem10  35905  prtlem15  36816  lshpcmp  36929  lsatn0  36940  lsatcmp  36944  lsmsat  36949  lsatcv0  36972  l1cvpat  36995  eqlkr  37040  lshpkrlem1  37051  lshpkrlem6  37056  lfl1dim  37062  lfl1dim2N  37063  lkrss2N  37110  athgt  37397  3dim2  37409  llnle  37459  llncmp  37463  lplnle  37481  lplnnle2at  37482  llncvrlpln2  37498  llncvrlpln  37499  lplncmp  37503  lplnexllnN  37505  lvolnle3at  37523  lplncvrlvol2  37556  lplncvrlvol  37557  lvolcmp  37558  pointpsubN  37692  pclfinN  37841  pclfinclN  37891  osumcllem11N  37907  pexmidlem4N  37914  cdleme17d3  38437  cdlemeg46gfre  38473  cdleme48gfv1  38477  cdleme50trn2  38492  trlord  38510  cdlemg6e  38563  cdlemj3  38764  diaelrnN  38986  diaintclN  38999  dia2dimlem6  39010  cdlemm10N  39059  dibintclN  39108  dihord6apre  39197  dihord5b  39200  dihord5apre  39203  dihglblem5apreN  39232  dihglblem2N  39235  dihglblem3N  39236  dihglbcpreN  39241  dihintcl  39285  lclkrlem2y  39472  lcfrvalsnN  39482  isnacs3  40448  jm2.26  40740  fnwe2lem2  40792  hbtlem5  40869  uzwo4  42490  iunincfi  42533  restuni3  42556  disjinfi  42620  ssnnf1octb  42622  choicefi  42629  mapssbi  42642  unirnmapsn  42643  ssmapsn  42645  iunmapsn  42646  supxrgere  42762  supxrgelem  42766  suplesup  42768  infleinf  42801  suplesup2  42805  rexabslelem  42848  islptre  43050  limcperiod  43059  limclner  43082  limsupmnfuzlem  43157  limsupre3lem  43163  coskpi2  43297  cosknegpi  43300  icccncfext  43318  stoweidlem27  43458  stoweidlem59  43490  fourierdlem41  43579  fourierdlem42  43580  fourierdlem70  43607  fourierdlem71  43608  fourierdlem81  43618  fourierswlem  43661  qndenserrnopnlem  43728  subsaliuncl  43787  subsalsal  43788  sge0tsms  43808  sge0fsum  43815  sge0supre  43817  sge0sup  43819  sge0rnbnd  43821  sge0pnffigt  43824  sge0resrn  43832  sge0split  43837  sge0iunmptlemfi  43841  sge0rpcpnf  43849  sge0isum  43855  sge0xaddlem2  43862  sge0uzfsumgt  43872  sge0seq  43874  sge0reuz  43875  nnfoctbdjlem  43883  nnfoctbdj  43884  meadjiunlem  43893  meaiuninclem  43908  carageniuncllem2  43950  caratheodorylem2  43955  ovnsupge0  43985  ovncvrrp  43992  hoidmv1lelem3  44021  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoilem2  44030  opnvonmbllem2  44061  ovolval5lem3  44082  ovnovollem3  44086  sssmf  44161  smfpimbor1lem1  44219  smfco  44223  smfpimcc  44228  smfinflem  44237  fmtno4prmfac  44912  sfprmdvdsmersenne  44943  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  bgoldbtbnd  45149