Theorem rexlimdv 3153

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  rexlimdva  3155  rexlimdva2  3157  rexlimdv3a  3159  rexlimdvw  3160  rexlimdvv  3212  rexlimdvvva  3214  elpwunsn  4684  onelssex  6432  eldmrexrnb  7112  weniso  7374  ssorduni  7799  onint  7810  limuni3  7873  peano5  7915  funcnvuni  7954  funeldmdif  8073  frxp  8151  smoiun  8401  tfrlem9  8425  oaordex  8596  oalimcl  8598  oaass  8599  findcard2  9204  findcard3  9318  findcard3OLD  9319  frfi  9321  unblem1  9328  ordiso2  9555  inf3lem3  9670  r1sdom  9814  tz9.12lem3  9829  karden  9935  infxpenlem  10053  cardinfima  10137  iunfictbso  10154  dfac5  10169  cfcoflem  10312  fin23lem11  10357  fin23lem30  10382  fin1a2lem13  10452  axdc3lem2  10491  konigthlem  10608  fpwwe2lem11  10681  tskuni  10823  axgroth6  10868  nqereu  10969  genpnmax  11047  ltaddpr  11074  recexsrlem  11143  mulgt0sr  11145  axrrecex  11203  axpre-sup  11209  addrid  11441  addlid  11444  recex  11895  btwnz  12721  lbzbi  12978  qbtwnre  13241  caubnd  15397  divalglem9  16438  unbenlem  16946  firest  17477  imasmnd2  18787  imasgrp2  19073  pmtrfrn  19476  pgpfi  19623  sylow2blem3  19640  imasrng  20174  imasring  20327  lspsneq  21124  lspdisj  21127  elcls  23081  elcls3  23091  subbascn  23262  cmpsublem  23407  cmpsub  23408  nllyidm  23497  comppfsc  23540  ptpjopn  23620  fbfinnfr  23849  filin  23862  isfil2  23864  infil  23871  fgss2  23882  fgfil  23883  fgcl  23886  fgabs  23887  elfm2  23956  rnelfm  23961  fmfnfmlem2  23963  fmfnfmlem4  23965  fmco  23969  flffbas  24003  cnpflf2  24008  fclscf  24033  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  alexsubALT  24059  neibl  24514  met2ndc  24536  metcnp3  24553  icccmplem2  24845  xrge0tsms  24856  fgcfil  25305  volfiniun  25582  dyadmax  25633  dyadmbllem  25634  c1liplem1  26035  dgrlem  26268  axcontlem10  28988  usgredg2vtxeuALT  29239  ushgredgedg  29246  ushgredgedgloop  29248  uhgrspan1  29320  nbuhgr2vtx1edgblem  29368  erclwwlksym  30040  erclwwlknsym  30089  1pthon2v  30172  conngrv2edg  30214  lpni  30499  grpoidinvlem3  30525  grporcan  30537  omlsii  31422  spansncol  31587  spansnss  31590  spanunsni  31598  h1datomi  31600  nmopsetretALT  31882  branmfn  32124  chjatom  32376  cvbr4i  32386  atomli  32401  xrge0tsmsd  33065  umgr2cycllem  35145  umgr2cycl  35146  sat1el2xp  35384  fmlasuc  35391  satffunlem1lem2  35408  satffunlem2lem1  35409  satffunlem2lem2  35411  dfon2lem6  35789  colineardim1  36062  finminlem  36319  nn0prpwlem  36323  neibastop2lem  36361  neibastop2  36362  fgmin  36371  exrecfnlem  37380  heiborlem10  37827  prtlem15  38876  lshpcmp  38989  lsatn0  39000  lsatcmp  39004  lsmsat  39009  lsatcv0  39032  l1cvpat  39055  eqlkr  39100  lshpkrlem1  39111  lshpkrlem6  39116  lfl1dim  39122  lfl1dim2N  39123  lkrss2N  39170  athgt  39458  3dim2  39470  llnle  39520  llncmp  39524  lplnle  39542  lplnnle2at  39543  llncvrlpln2  39559  llncvrlpln  39560  lplncmp  39564  lplnexllnN  39566  lvolnle3at  39584  lplncvrlvol2  39617  lplncvrlvol  39618  lvolcmp  39619  pointpsubN  39753  pclfinN  39902  pclfinclN  39952  osumcllem11N  39968  pexmidlem4N  39975  cdleme17d3  40498  cdlemeg46gfre  40534  cdleme48gfv1  40538  cdleme50trn2  40553  trlord  40571  cdlemg6e  40624  cdlemj3  40825  diaelrnN  41047  diaintclN  41060  dia2dimlem6  41071  cdlemm10N  41120  dibintclN  41169  dihord6apre  41258  dihord5b  41261  dihord5apre  41264  dihglblem5apreN  41293  dihglblem2N  41296  dihglblem3N  41297  dihglbcpreN  41302  dihintcl  41346  lclkrlem2y  41533  lcfrvalsnN  41543  isnacs3  42721  jm2.26  43014  fnwe2lem2  43063  hbtlem5  43140  dflim5  43342  uzwo4  45058  iunincfi  45099  restuni3  45123  disjinfi  45197  ssnnf1octb  45199  choicefi  45205  mapssbi  45218  unirnmapsn  45219  iunmapsn  45222  supxrgere  45344  supxrgelem  45348  suplesup  45350  infleinf  45383  suplesup2  45387  rexabslelem  45429  islptre  45634  limcperiod  45643  limclner  45666  limsupmnfuzlem  45741  limsupre3lem  45747  coskpi2  45881  cosknegpi  45884  icccncfext  45902  stoweidlem27  46042  stoweidlem59  46074  fourierdlem41  46163  fourierdlem42  46164  fourierdlem70  46191  fourierdlem71  46192  fourierdlem81  46202  fourierswlem  46245  qndenserrnopnlem  46312  subsaliuncl  46373  subsalsal  46374  sge0tsms  46395  sge0fsum  46402  sge0supre  46404  sge0sup  46406  sge0rnbnd  46408  sge0pnffigt  46411  sge0resrn  46419  sge0split  46424  sge0iunmptlemfi  46428  sge0rpcpnf  46436  sge0isum  46442  sge0xaddlem2  46449  sge0uzfsumgt  46459  sge0seq  46461  sge0reuz  46462  nnfoctbdjlem  46470  nnfoctbdj  46471  meadjiunlem  46480  meaiuninclem  46495  carageniuncllem2  46537  caratheodorylem2  46542  ovnsupge0  46572  ovncvrrp  46579  hoidmv1lelem3  46608  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnhoilem2  46617  opnvonmbllem2  46648  ovnovollem3  46673  sssmf  46753  smfpimbor1lem1  46813  smfco  46817  smfpimcc  46823  smfinflem  46832  fmtno4prmfac  47559  sfprmdvdsmersenne  47590  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  bgoldbtbnd  47796  grimuhgr  47878  clnbgrgrim  47902  uspgrlimlem2  47956