Theorem rexlimdv 3170

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

Syntax hints:   → wi 4   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  rexlimdva  3172  rexlimdva2  3174  rexlimdv3a  3176  rexlimdvw  3177  rexlimdvv  3227  rexlimdvvva  3229  elpwunsn  4652  onelssex  6407  eldmrexrnb  7085  weniso  7350  ssorduni  7774  onint  7785  limuni3  7844  peano5  7886  funcnvuni  7925  funeldmdif  8041  frxp  8118  smoiun  8344  tfrlem9  8368  oaordex  8539  oalimcl  8541  oaass  8542  findcard2  9145  findcard3  9239  frfi  9241  unblem1  9248  ordiso2  9473  inf3lem3  9595  r1sdom  9742  tz9.12lem3  9757  karden  9877  infxpenlem  9993  cardinfima  10077  iunfictbso  10094  dfac5  10108  cfcoflem  10252  fin23lem11  10297  fin23lem30  10322  fin1a2lem13  10392  axdc3lem2  10431  konigthlem  10549  fpwwe2lem11  10622  tskuni  10764  axgroth6  10809  nqereu  10910  genpnmax  10988  ltaddpr  11015  recexsrlem  11084  mulgt0sr  11086  axrrecex  11144  axpre-sup  11150  addrid  11386  addlid  11389  recex  11842  btwnz  12695  lbzbi  12956  qbtwnre  13221  caubnd  15406  divalglem9  16455  unbenlem  16964  firest  17481  imasmnd2  18828  imasgrp2  19117  pmtrfrn  19524  pgpfi  19671  sylow2blem3  19688  imasrng  20251  imasring  20408  lspsneq  21220  lspdisj  21223  elcls  23195  elcls3  23205  subbascn  23376  cmpsublem  23521  cmpsub  23522  nllyidm  23611  comppfsc  23654  ptpjopn  23734  fbfinnfr  23963  filin  23976  isfil2  23978  infil  23985  fgss2  23996  fgfil  23997  fgcl  24000  fgabs  24001  elfm2  24070  rnelfm  24075  fmfnfmlem2  24077  fmfnfmlem4  24079  fmco  24083  flffbas  24117  cnpflf2  24122  fclscf  24147  alexsubALTlem2  24170  alexsubALTlem3  24171  alexsubALTlem4  24172  alexsubALT  24173  neibl  24623  met2ndc  24645  metcnp3  24662  icccmplem2  24946  xrge0tsms  24957  fgcfil  25395  volfiniun  25671  dyadmax  25722  dyadmbllem  25723  c1liplem1  26120  dgrlem  26351  axcontlem10  29260  usgredg2vtxeuALT  29509  ushgredgedg  29516  ushgredgedgloop  29518  uhgrspan1  29590  nbuhgr2vtx1edgblem  29638  erclwwlksym  30309  erclwwlknsym  30358  1pthon2v  30441  conngrv2edg  30483  lpni  30769  grpoidinvlem3  30795  grporcan  30807  omlsii  31692  spansncol  31857  spansnss  31860  spanunsni  31868  h1datomi  31870  nmopsetretALT  32152  branmfn  32394  chjatom  32646  cvbr4i  32656  atomli  32671  xrge0tsmsd  33330  umgr2cycllem  35527  umgr2cycl  35528  sat1el2xp  35766  fmlasuc  35773  satffunlem1lem2  35790  satffunlem2lem1  35791  satffunlem2lem2  35793  dfon2lem6  36173  colineardim1  36448  finminlem  36714  nn0prpwlem  36718  neibastop2lem  36756  neibastop2  36757  fgmin  36766  exrecfnlem  37908  heiborlem10  38354  prtlem15  39534  lshpcmp  39647  lsatn0  39658  lsatcmp  39662  lsmsat  39667  lsatcv0  39690  l1cvpat  39713  eqlkr  39758  lshpkrlem1  39769  lshpkrlem6  39774  lfl1dim  39780  lfl1dim2N  39781  lkrss2N  39828  athgt  40115  3dim2  40127  llnle  40177  llncmp  40181  lplnle  40199  lplnnle2at  40200  llncvrlpln2  40216  llncvrlpln  40217  lplncmp  40221  lplnexllnN  40223  lvolnle3at  40241  lplncvrlvol2  40274  lplncvrlvol  40275  lvolcmp  40276  pointpsubN  40410  pclfinN  40559  pclfinclN  40609  osumcllem11N  40625  pexmidlem4N  40632  cdleme17d3  41155  cdlemeg46gfre  41191  cdleme48gfv1  41195  cdleme50trn2  41210  trlord  41228  cdlemg6e  41281  cdlemj3  41482  diaelrnN  41704  diaintclN  41717  dia2dimlem6  41728  cdlemm10N  41777  dibintclN  41826  dihord6apre  41915  dihord5b  41918  dihord5apre  41921  dihglblem5apreN  41950  dihglblem2N  41953  dihglblem3N  41954  dihglbcpreN  41959  dihintcl  42003  lclkrlem2y  42190  lcfrvalsnN  42200  isnacs3  43326  jm2.26  43614  fnwe2lem2  43663  hbtlem5  43740  dflim5  43941  uzwo4  45658  iunincfi  45697  restuni3  45721  disjinfi  45795  ssnnf1octb  45797  choicefi  45802  mapssbi  45814  unirnmapsn  45815  iunmapsn  45818  supxrgere  45934  supxrgelem  45938  suplesup  45940  infleinf  45972  suplesup2  45976  rexabslelem  46017  islptre  46220  limcperiod  46229  limclner  46250  limsupmnfuzlem  46325  limsupre3lem  46331  coskpi2  46465  cosknegpi  46468  icccncfext  46486  stoweidlem27  46626  stoweidlem59  46658  fourierdlem41  46747  fourierdlem42  46748  fourierdlem70  46775  fourierdlem71  46776  fourierdlem81  46786  fourierswlem  46829  qndenserrnopnlem  46896  subsaliuncl  46957  subsalsal  46958  sge0tsms  46979  sge0fsum  46986  sge0supre  46988  sge0sup  46990  sge0rnbnd  46992  sge0pnffigt  46995  sge0resrn  47003  sge0split  47008  sge0iunmptlemfi  47012  sge0rpcpnf  47020  sge0isum  47026  sge0xaddlem2  47033  sge0uzfsumgt  47043  sge0seq  47045  sge0reuz  47046  nnfoctbdjlem  47054  nnfoctbdj  47055  meadjiunlem  47064  meaiuninclem  47079  carageniuncllem2  47121  caratheodorylem2  47126  ovnsupge0  47156  ovncvrrp  47163  hoidmv1lelem3  47192  hoidmv1le  47193  hoidmvlelem1  47194  hoidmvlelem2  47195  hoidmvlelem3  47196  ovnhoilem2  47201  opnvonmbllem2  47232  ovnovollem3  47257  smfpimbor1lem1  47397  smfco  47401  smfpimcc  47407  smfinflem  47416  nprmmul3  48160  fmtno4prmfac  48206  sfprmdvdsmersenne  48237  nnsum4primeseven  48447  nnsum4primesevenALTV  48448  bgoldbtbnd  48456  grimuhgr  48534  clnbgrgrim  48581  uspgrlimlem2  48636