Theorem rexlimdv 3140

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-rex 3060

This theorem is referenced by:  rexlimdva  3142  rexlimdva2  3144  rexlimdv3a  3146  rexlimdvw  3147  rexlimdvv  3199  rexlimdvvva  3201  elpwunsn  4664  onelssex  6412  eldmrexrnb  7092  weniso  7356  ssorduni  7781  onint  7792  limuni3  7855  peano5  7897  funcnvuni  7936  funeldmdif  8055  frxp  8133  smoiun  8383  tfrlem9  8407  oaordex  8578  oalimcl  8580  oaass  8581  findcard2  9186  findcard3  9300  findcard3OLD  9301  frfi  9303  unblem1  9310  ordiso2  9537  inf3lem3  9652  r1sdom  9796  tz9.12lem3  9811  karden  9917  infxpenlem  10035  cardinfima  10119  iunfictbso  10136  dfac5  10151  cfcoflem  10294  fin23lem11  10339  fin23lem30  10364  fin1a2lem13  10434  axdc3lem2  10473  konigthlem  10590  fpwwe2lem11  10663  tskuni  10805  axgroth6  10850  nqereu  10951  genpnmax  11029  ltaddpr  11056  recexsrlem  11125  mulgt0sr  11127  axrrecex  11185  axpre-sup  11191  addrid  11423  addlid  11426  recex  11877  btwnz  12704  lbzbi  12960  qbtwnre  13223  caubnd  15379  divalglem9  16420  unbenlem  16928  firest  17448  imasmnd2  18756  imasgrp2  19042  pmtrfrn  19444  pgpfi  19591  sylow2blem3  19608  imasrng  20142  imasring  20295  lspsneq  21092  lspdisj  21095  elcls  23027  elcls3  23037  subbascn  23208  cmpsublem  23353  cmpsub  23354  nllyidm  23443  comppfsc  23486  ptpjopn  23566  fbfinnfr  23795  filin  23808  isfil2  23810  infil  23817  fgss2  23828  fgfil  23829  fgcl  23832  fgabs  23833  elfm2  23902  rnelfm  23907  fmfnfmlem2  23909  fmfnfmlem4  23911  fmco  23915  flffbas  23949  cnpflf2  23954  fclscf  23979  alexsubALTlem2  24002  alexsubALTlem3  24003  alexsubALTlem4  24004  alexsubALT  24005  neibl  24458  met2ndc  24480  metcnp3  24497  icccmplem2  24781  xrge0tsms  24792  fgcfil  25241  volfiniun  25518  dyadmax  25569  dyadmbllem  25570  c1liplem1  25971  dgrlem  26204  axcontlem10  28918  usgredg2vtxeuALT  29167  ushgredgedg  29174  ushgredgedgloop  29176  uhgrspan1  29248  nbuhgr2vtx1edgblem  29296  erclwwlksym  29968  erclwwlknsym  30017  1pthon2v  30100  conngrv2edg  30142  lpni  30427  grpoidinvlem3  30453  grporcan  30465  omlsii  31350  spansncol  31515  spansnss  31518  spanunsni  31526  h1datomi  31528  nmopsetretALT  31810  branmfn  32052  chjatom  32304  cvbr4i  32314  atomli  32329  xrge0tsmsd  33004  umgr2cycllem  35104  umgr2cycl  35105  sat1el2xp  35343  fmlasuc  35350  satffunlem1lem2  35367  satffunlem2lem1  35368  satffunlem2lem2  35370  dfon2lem6  35748  colineardim1  36021  finminlem  36278  nn0prpwlem  36282  neibastop2lem  36320  neibastop2  36321  fgmin  36330  exrecfnlem  37339  heiborlem10  37786  prtlem15  38835  lshpcmp  38948  lsatn0  38959  lsatcmp  38963  lsmsat  38968  lsatcv0  38991  l1cvpat  39014  eqlkr  39059  lshpkrlem1  39070  lshpkrlem6  39075  lfl1dim  39081  lfl1dim2N  39082  lkrss2N  39129  athgt  39417  3dim2  39429  llnle  39479  llncmp  39483  lplnle  39501  lplnnle2at  39502  llncvrlpln2  39518  llncvrlpln  39519  lplncmp  39523  lplnexllnN  39525  lvolnle3at  39543  lplncvrlvol2  39576  lplncvrlvol  39577  lvolcmp  39578  pointpsubN  39712  pclfinN  39861  pclfinclN  39911  osumcllem11N  39927  pexmidlem4N  39934  cdleme17d3  40457  cdlemeg46gfre  40493  cdleme48gfv1  40497  cdleme50trn2  40512  trlord  40530  cdlemg6e  40583  cdlemj3  40784  diaelrnN  41006  diaintclN  41019  dia2dimlem6  41030  cdlemm10N  41079  dibintclN  41128  dihord6apre  41217  dihord5b  41220  dihord5apre  41223  dihglblem5apreN  41252  dihglblem2N  41255  dihglblem3N  41256  dihglbcpreN  41261  dihintcl  41305  lclkrlem2y  41492  lcfrvalsnN  41502  isnacs3  42684  jm2.26  42977  fnwe2lem2  43026  hbtlem5  43103  dflim5  43304  uzwo4  45015  iunincfi  45056  restuni3  45080  disjinfi  45154  ssnnf1octb  45156  choicefi  45162  mapssbi  45175  unirnmapsn  45176  iunmapsn  45179  supxrgere  45301  supxrgelem  45305  suplesup  45307  infleinf  45340  suplesup2  45344  rexabslelem  45386  islptre  45591  limcperiod  45600  limclner  45623  limsupmnfuzlem  45698  limsupre3lem  45704  coskpi2  45838  cosknegpi  45841  icccncfext  45859  stoweidlem27  45999  stoweidlem59  46031  fourierdlem41  46120  fourierdlem42  46121  fourierdlem70  46148  fourierdlem71  46149  fourierdlem81  46159  fourierswlem  46202  qndenserrnopnlem  46269  subsaliuncl  46330  subsalsal  46331  sge0tsms  46352  sge0fsum  46359  sge0supre  46361  sge0sup  46363  sge0rnbnd  46365  sge0pnffigt  46368  sge0resrn  46376  sge0split  46381  sge0iunmptlemfi  46385  sge0rpcpnf  46393  sge0isum  46399  sge0xaddlem2  46406  sge0uzfsumgt  46416  sge0seq  46418  sge0reuz  46419  nnfoctbdjlem  46427  nnfoctbdj  46428  meadjiunlem  46437  meaiuninclem  46452  carageniuncllem2  46494  caratheodorylem2  46499  ovnsupge0  46529  ovncvrrp  46536  hoidmv1lelem3  46565  hoidmv1le  46566  hoidmvlelem1  46567  hoidmvlelem2  46568  hoidmvlelem3  46569  ovnhoilem2  46574  opnvonmbllem2  46605  ovnovollem3  46630  sssmf  46710  smfpimbor1lem1  46770  smfco  46774  smfpimcc  46780  smfinflem  46789  fmtno4prmfac  47517  sfprmdvdsmersenne  47548  nnsum4primeseven  47745  nnsum4primesevenALTV  47746  bgoldbtbnd  47754  grimuhgr  47836  clnbgrgrim  47860  uspgrlimlem2  47914