Theorem rexlimdv 3160

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 3155	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 → (𝜑 → 𝜒))
4	3	com12 32	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  rexlimdva  3162  rexlimdva2  3164  rexlimdv3a  3166  rexlimdvw  3167  rexlimdvv  3217  rexlimdvvva  3219  elpwunsn  4640  onelssex  6389  eldmrexrnb  7067  weniso  7332  ssorduni  7756  onint  7767  limuni3  7826  peano5  7868  funcnvuni  7907  funeldmdif  8023  frxp  8099  smoiun  8325  tfrlem9  8349  oaordex  8520  oalimcl  8522  oaass  8523  findcard2  9126  findcard3  9220  frfi  9222  unblem1  9229  ordiso2  9456  inf3lem3  9578  r1sdom  9725  tz9.12lem3  9740  karden  9846  infxpenlem  9962  cardinfima  10046  iunfictbso  10063  dfac5  10078  cfcoflem  10222  fin23lem11  10267  fin23lem30  10292  fin1a2lem13  10362  axdc3lem2  10401  konigthlem  10519  fpwwe2lem11  10592  tskuni  10734  axgroth6  10779  nqereu  10880  genpnmax  10958  ltaddpr  10985  recexsrlem  11054  mulgt0sr  11056  axrrecex  11114  axpre-sup  11120  addrid  11356  addlid  11359  recex  11812  btwnz  12669  lbzbi  12930  qbtwnre  13195  caubnd  15376  divalglem9  16425  unbenlem  16934  firest  17451  imasmnd2  18798  imasgrp2  19087  pmtrfrn  19488  pgpfi  19635  sylow2blem3  19652  imasrng  20213  imasring  20365  lspsneq  21179  lspdisj  21182  elcls  23120  elcls3  23130  subbascn  23301  cmpsublem  23446  cmpsub  23447  nllyidm  23536  comppfsc  23579  ptpjopn  23659  fbfinnfr  23888  filin  23901  isfil2  23903  infil  23910  fgss2  23921  fgfil  23922  fgcl  23925  fgabs  23926  elfm2  23995  rnelfm  24000  fmfnfmlem2  24002  fmfnfmlem4  24004  fmco  24008  flffbas  24042  cnpflf2  24047  fclscf  24072  alexsubALTlem2  24095  alexsubALTlem3  24096  alexsubALTlem4  24097  alexsubALT  24098  neibl  24548  met2ndc  24570  metcnp3  24587  icccmplem2  24871  xrge0tsms  24882  fgcfil  25320  volfiniun  25596  dyadmax  25647  dyadmbllem  25648  c1liplem1  26045  dgrlem  26276  axcontlem10  29130  usgredg2vtxeuALT  29379  ushgredgedg  29386  ushgredgedgloop  29388  uhgrspan1  29460  nbuhgr2vtx1edgblem  29508  erclwwlksym  30179  erclwwlknsym  30228  1pthon2v  30311  conngrv2edg  30353  lpni  30639  grpoidinvlem3  30665  grporcan  30677  omlsii  31562  spansncol  31727  spansnss  31730  spanunsni  31738  h1datomi  31740  nmopsetretALT  32022  branmfn  32264  chjatom  32516  cvbr4i  32526  atomli  32541  xrge0tsmsd  33213  umgr2cycllem  35450  umgr2cycl  35451  sat1el2xp  35689  fmlasuc  35696  satffunlem1lem2  35713  satffunlem2lem1  35714  satffunlem2lem2  35716  dfon2lem6  36096  colineardim1  36371  finminlem  36638  nn0prpwlem  36642  neibastop2lem  36680  neibastop2  36681  fgmin  36690  exrecfnlem  37833  heiborlem10  38279  prtlem15  39459  lshpcmp  39572  lsatn0  39583  lsatcmp  39587  lsmsat  39592  lsatcv0  39615  l1cvpat  39638  eqlkr  39683  lshpkrlem1  39694  lshpkrlem6  39699  lfl1dim  39705  lfl1dim2N  39706  lkrss2N  39753  athgt  40040  3dim2  40052  llnle  40102  llncmp  40106  lplnle  40124  lplnnle2at  40125  llncvrlpln2  40141  llncvrlpln  40142  lplncmp  40146  lplnexllnN  40148  lvolnle3at  40166  lplncvrlvol2  40199  lplncvrlvol  40200  lvolcmp  40201  pointpsubN  40335  pclfinN  40484  pclfinclN  40534  osumcllem11N  40550  pexmidlem4N  40557  cdleme17d3  41080  cdlemeg46gfre  41116  cdleme48gfv1  41120  cdleme50trn2  41135  trlord  41153  cdlemg6e  41206  cdlemj3  41407  diaelrnN  41629  diaintclN  41642  dia2dimlem6  41653  cdlemm10N  41702  dibintclN  41751  dihord6apre  41840  dihord5b  41843  dihord5apre  41846  dihglblem5apreN  41875  dihglblem2N  41878  dihglblem3N  41879  dihglbcpreN  41884  dihintcl  41928  lclkrlem2y  42115  lcfrvalsnN  42125  isnacs3  43251  jm2.26  43539  fnwe2lem2  43588  hbtlem5  43665  dflim5  43866  uzwo4  45593  iunincfi  45632  restuni3  45656  disjinfi  45730  ssnnf1octb  45732  choicefi  45737  mapssbi  45749  unirnmapsn  45750  iunmapsn  45753  supxrgere  45869  supxrgelem  45873  suplesup  45875  infleinf  45907  suplesup2  45911  rexabslelem  45952  islptre  46155  limcperiod  46164  limclner  46185  limsupmnfuzlem  46260  limsupre3lem  46266  coskpi2  46400  cosknegpi  46403  icccncfext  46421  stoweidlem27  46561  stoweidlem59  46593  fourierdlem41  46682  fourierdlem42  46683  fourierdlem70  46710  fourierdlem71  46711  fourierdlem81  46721  fourierswlem  46764  qndenserrnopnlem  46831  subsaliuncl  46892  subsalsal  46893  sge0tsms  46914  sge0fsum  46921  sge0supre  46923  sge0sup  46925  sge0rnbnd  46927  sge0pnffigt  46930  sge0resrn  46938  sge0split  46943  sge0iunmptlemfi  46947  sge0rpcpnf  46955  sge0isum  46961  sge0xaddlem2  46968  sge0uzfsumgt  46978  sge0seq  46980  sge0reuz  46981  nnfoctbdjlem  46989  nnfoctbdj  46990  meadjiunlem  46999  meaiuninclem  47014  carageniuncllem2  47056  caratheodorylem2  47061  ovnsupge0  47091  ovncvrrp  47098  hoidmv1lelem3  47127  hoidmv1le  47128  hoidmvlelem1  47129  hoidmvlelem2  47130  hoidmvlelem3  47131  ovnhoilem2  47136  opnvonmbllem2  47167  ovnovollem3  47192  smfpimbor1lem1  47332  smfco  47336  smfpimcc  47342  smfinflem  47351  nprmmul3  48095  fmtno4prmfac  48141  sfprmdvdsmersenne  48172  nnsum4primeseven  48382  nnsum4primesevenALTV  48383  bgoldbtbnd  48391  grimuhgr  48469  clnbgrgrim  48516  uspgrlimlem2  48571