Theorem rexlimdv 3139

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

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

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 3061

This theorem is referenced by:  rexlimdva  3141  rexlimdva2  3143  rexlimdv3a  3145  rexlimdvw  3146  rexlimdvv  3197  rexlimdvvva  3199  elpwunsn  4660  onelssex  6401  eldmrexrnb  7081  weniso  7346  ssorduni  7771  onint  7782  limuni3  7845  peano5  7887  funcnvuni  7926  funeldmdif  8045  frxp  8123  smoiun  8373  tfrlem9  8397  oaordex  8568  oalimcl  8570  oaass  8571  findcard2  9176  findcard3  9288  findcard3OLD  9289  frfi  9291  unblem1  9298  ordiso2  9527  inf3lem3  9642  r1sdom  9786  tz9.12lem3  9801  karden  9907  infxpenlem  10025  cardinfima  10109  iunfictbso  10126  dfac5  10141  cfcoflem  10284  fin23lem11  10329  fin23lem30  10354  fin1a2lem13  10424  axdc3lem2  10463  konigthlem  10580  fpwwe2lem11  10653  tskuni  10795  axgroth6  10840  nqereu  10941  genpnmax  11019  ltaddpr  11046  recexsrlem  11115  mulgt0sr  11117  axrrecex  11175  axpre-sup  11181  addrid  11413  addlid  11416  recex  11867  btwnz  12694  lbzbi  12950  qbtwnre  13213  caubnd  15375  divalglem9  16418  unbenlem  16926  firest  17444  imasmnd2  18750  imasgrp2  19036  pmtrfrn  19437  pgpfi  19584  sylow2blem3  19601  imasrng  20135  imasring  20288  lspsneq  21081  lspdisj  21084  elcls  23009  elcls3  23019  subbascn  23190  cmpsublem  23335  cmpsub  23336  nllyidm  23425  comppfsc  23468  ptpjopn  23548  fbfinnfr  23777  filin  23790  isfil2  23792  infil  23799  fgss2  23810  fgfil  23811  fgcl  23814  fgabs  23815  elfm2  23884  rnelfm  23889  fmfnfmlem2  23891  fmfnfmlem4  23893  fmco  23897  flffbas  23931  cnpflf2  23936  fclscf  23961  alexsubALTlem2  23984  alexsubALTlem3  23985  alexsubALTlem4  23986  alexsubALT  23987  neibl  24438  met2ndc  24460  metcnp3  24477  icccmplem2  24761  xrge0tsms  24772  fgcfil  25221  volfiniun  25498  dyadmax  25549  dyadmbllem  25550  c1liplem1  25951  dgrlem  26184  axcontlem10  28898  usgredg2vtxeuALT  29147  ushgredgedg  29154  ushgredgedgloop  29156  uhgrspan1  29228  nbuhgr2vtx1edgblem  29276  erclwwlksym  29948  erclwwlknsym  29997  1pthon2v  30080  conngrv2edg  30122  lpni  30407  grpoidinvlem3  30433  grporcan  30445  omlsii  31330  spansncol  31495  spansnss  31498  spanunsni  31506  h1datomi  31508  nmopsetretALT  31790  branmfn  32032  chjatom  32284  cvbr4i  32294  atomli  32309  xrge0tsmsd  33002  umgr2cycllem  35108  umgr2cycl  35109  sat1el2xp  35347  fmlasuc  35354  satffunlem1lem2  35371  satffunlem2lem1  35372  satffunlem2lem2  35374  dfon2lem6  35752  colineardim1  36025  finminlem  36282  nn0prpwlem  36286  neibastop2lem  36324  neibastop2  36325  fgmin  36334  exrecfnlem  37343  heiborlem10  37790  prtlem15  38839  lshpcmp  38952  lsatn0  38963  lsatcmp  38967  lsmsat  38972  lsatcv0  38995  l1cvpat  39018  eqlkr  39063  lshpkrlem1  39074  lshpkrlem6  39079  lfl1dim  39085  lfl1dim2N  39086  lkrss2N  39133  athgt  39421  3dim2  39433  llnle  39483  llncmp  39487  lplnle  39505  lplnnle2at  39506  llncvrlpln2  39522  llncvrlpln  39523  lplncmp  39527  lplnexllnN  39529  lvolnle3at  39547  lplncvrlvol2  39580  lplncvrlvol  39581  lvolcmp  39582  pointpsubN  39716  pclfinN  39865  pclfinclN  39915  osumcllem11N  39931  pexmidlem4N  39938  cdleme17d3  40461  cdlemeg46gfre  40497  cdleme48gfv1  40501  cdleme50trn2  40516  trlord  40534  cdlemg6e  40587  cdlemj3  40788  diaelrnN  41010  diaintclN  41023  dia2dimlem6  41034  cdlemm10N  41083  dibintclN  41132  dihord6apre  41221  dihord5b  41224  dihord5apre  41227  dihglblem5apreN  41256  dihglblem2N  41259  dihglblem3N  41260  dihglbcpreN  41265  dihintcl  41309  lclkrlem2y  41496  lcfrvalsnN  41506  isnacs3  42680  jm2.26  42973  fnwe2lem2  43022  hbtlem5  43099  dflim5  43300  uzwo4  45025  iunincfi  45066  restuni3  45090  disjinfi  45164  ssnnf1octb  45166  choicefi  45172  mapssbi  45185  unirnmapsn  45186  iunmapsn  45189  supxrgere  45308  supxrgelem  45312  suplesup  45314  infleinf  45347  suplesup2  45351  rexabslelem  45393  islptre  45596  limcperiod  45605  limclner  45628  limsupmnfuzlem  45703  limsupre3lem  45709  coskpi2  45843  cosknegpi  45846  icccncfext  45864  stoweidlem27  46004  stoweidlem59  46036  fourierdlem41  46125  fourierdlem42  46126  fourierdlem70  46153  fourierdlem71  46154  fourierdlem81  46164  fourierswlem  46207  qndenserrnopnlem  46274  subsaliuncl  46335  subsalsal  46336  sge0tsms  46357  sge0fsum  46364  sge0supre  46366  sge0sup  46368  sge0rnbnd  46370  sge0pnffigt  46373  sge0resrn  46381  sge0split  46386  sge0iunmptlemfi  46390  sge0rpcpnf  46398  sge0isum  46404  sge0xaddlem2  46411  sge0uzfsumgt  46421  sge0seq  46423  sge0reuz  46424  nnfoctbdjlem  46432  nnfoctbdj  46433  meadjiunlem  46442  meaiuninclem  46457  carageniuncllem2  46499  caratheodorylem2  46504  ovnsupge0  46534  ovncvrrp  46541  hoidmv1lelem3  46570  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  ovnhoilem2  46579  opnvonmbllem2  46610  ovnovollem3  46635  sssmf  46715  smfpimbor1lem1  46775  smfco  46779  smfpimcc  46785  smfinflem  46794  fmtno4prmfac  47534  sfprmdvdsmersenne  47565  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  bgoldbtbnd  47771  grimuhgr  47848  clnbgrgrim  47895  uspgrlimlem2  47949