Theorem rexlimdv 3145

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

Syntax hints:   → wi 4   ∈ wcel 2098  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-rex 3063

This theorem is referenced by:  rexlimdva  3147  rexlimdva2  3149  rexlimdv3a  3151  rexlimdvw  3152  rexlimdvv  3202  elpwunsn  4679  onelssex  6402  eldmrexrnb  7083  weniso  7343  ssorduni  7759  onint  7771  limuni3  7834  peano5  7877  funcnvuni  7915  funeldmdif  8027  frxp  8106  smoiun  8356  tfrlem9  8380  oaordex  8553  oalimcl  8555  oaass  8556  findcard2  9159  findcard3  9280  findcard3OLD  9281  frfi  9283  unblem1  9290  ordiso2  9505  inf3lem3  9620  r1sdom  9764  tz9.12lem3  9779  karden  9885  infxpenlem  10003  cardinfima  10087  iunfictbso  10104  dfac5  10118  cfcoflem  10262  fin23lem11  10307  fin23lem30  10332  fin1a2lem13  10402  axdc3lem2  10441  konigthlem  10558  fpwwe2lem11  10631  tskuni  10773  axgroth6  10818  nqereu  10919  genpnmax  10997  ltaddpr  11024  recexsrlem  11093  mulgt0sr  11095  axrrecex  11153  axpre-sup  11159  addrid  11390  addlid  11393  recex  11842  btwnz  12661  lbzbi  12916  qbtwnre  13174  caubnd  15301  divalglem9  16340  unbenlem  16839  firest  17376  imasmnd2  18693  imasgrp2  18972  pmtrfrn  19367  pgpfi  19514  sylow2blem3  19531  imasrng  20071  imasring  20218  lspsneq  20962  lspdisj  20965  elcls  22898  elcls3  22908  subbascn  23079  cmpsublem  23224  cmpsub  23225  nllyidm  23314  comppfsc  23357  ptpjopn  23437  fbfinnfr  23666  filin  23679  isfil2  23681  infil  23688  fgss2  23699  fgfil  23700  fgcl  23703  fgabs  23704  elfm2  23773  rnelfm  23778  fmfnfmlem2  23780  fmfnfmlem4  23782  fmco  23786  flffbas  23820  cnpflf2  23825  fclscf  23850  alexsubALTlem2  23873  alexsubALTlem3  23874  alexsubALTlem4  23875  alexsubALT  23876  neibl  24331  met2ndc  24353  metcnp3  24370  icccmplem2  24660  xrge0tsms  24671  fgcfil  25120  volfiniun  25397  dyadmax  25448  dyadmbllem  25449  c1liplem1  25850  dgrlem  26082  axcontlem10  28666  usgredg2vtxeuALT  28914  ushgredgedg  28921  ushgredgedgloop  28923  uhgrspan1  28995  nbuhgr2vtx1edgblem  29043  erclwwlksym  29709  erclwwlknsym  29758  1pthon2v  29841  conngrv2edg  29883  lpni  30168  grpoidinvlem3  30194  grporcan  30206  omlsii  31091  spansncol  31256  spansnss  31259  spanunsni  31267  h1datomi  31269  nmopsetretALT  31551  branmfn  31793  chjatom  32045  cvbr4i  32055  atomli  32070  xrge0tsmsd  32643  umgr2cycllem  34586  umgr2cycl  34587  sat1el2xp  34825  fmlasuc  34832  satffunlem1lem2  34849  satffunlem2lem1  34850  satffunlem2lem2  34852  dfon2lem6  35221  colineardim1  35494  finminlem  35659  nn0prpwlem  35663  neibastop2lem  35701  neibastop2  35702  fgmin  35711  exrecfnlem  36716  heiborlem10  37144  prtlem15  38201  lshpcmp  38314  lsatn0  38325  lsatcmp  38329  lsmsat  38334  lsatcv0  38357  l1cvpat  38380  eqlkr  38425  lshpkrlem1  38436  lshpkrlem6  38441  lfl1dim  38447  lfl1dim2N  38448  lkrss2N  38495  athgt  38783  3dim2  38795  llnle  38845  llncmp  38849  lplnle  38867  lplnnle2at  38868  llncvrlpln2  38884  llncvrlpln  38885  lplncmp  38889  lplnexllnN  38891  lvolnle3at  38909  lplncvrlvol2  38942  lplncvrlvol  38943  lvolcmp  38944  pointpsubN  39078  pclfinN  39227  pclfinclN  39277  osumcllem11N  39293  pexmidlem4N  39300  cdleme17d3  39823  cdlemeg46gfre  39859  cdleme48gfv1  39863  cdleme50trn2  39878  trlord  39896  cdlemg6e  39949  cdlemj3  40150  diaelrnN  40372  diaintclN  40385  dia2dimlem6  40396  cdlemm10N  40445  dibintclN  40494  dihord6apre  40583  dihord5b  40586  dihord5apre  40589  dihglblem5apreN  40618  dihglblem2N  40621  dihglblem3N  40622  dihglbcpreN  40627  dihintcl  40671  lclkrlem2y  40858  lcfrvalsnN  40868  isnacs3  41903  jm2.26  42196  fnwe2lem2  42248  hbtlem5  42325  dflim5  42534  uzwo4  44194  iunincfi  44237  restuni3  44261  disjinfi  44342  ssnnf1octb  44344  choicefi  44350  mapssbi  44363  unirnmapsn  44364  ssmapsn  44366  iunmapsn  44367  supxrgere  44494  supxrgelem  44498  suplesup  44500  infleinf  44533  suplesup2  44537  rexabslelem  44579  islptre  44786  limcperiod  44795  limclner  44818  limsupmnfuzlem  44893  limsupre3lem  44899  coskpi2  45033  cosknegpi  45036  icccncfext  45054  stoweidlem27  45194  stoweidlem59  45226  fourierdlem41  45315  fourierdlem42  45316  fourierdlem70  45343  fourierdlem71  45344  fourierdlem81  45354  fourierswlem  45397  qndenserrnopnlem  45464  subsaliuncl  45525  subsalsal  45526  sge0tsms  45547  sge0fsum  45554  sge0supre  45556  sge0sup  45558  sge0rnbnd  45560  sge0pnffigt  45563  sge0resrn  45571  sge0split  45576  sge0iunmptlemfi  45580  sge0rpcpnf  45588  sge0isum  45594  sge0xaddlem2  45601  sge0uzfsumgt  45611  sge0seq  45613  sge0reuz  45614  nnfoctbdjlem  45622  nnfoctbdj  45623  meadjiunlem  45632  meaiuninclem  45647  carageniuncllem2  45689  caratheodorylem2  45694  ovnsupge0  45724  ovncvrrp  45731  hoidmv1lelem3  45760  hoidmv1le  45761  hoidmvlelem1  45762  hoidmvlelem2  45763  hoidmvlelem3  45764  ovnhoilem2  45769  opnvonmbllem2  45800  ovnovollem3  45825  sssmf  45905  smfpimbor1lem1  45965  smfco  45969  smfpimcc  45975  smfinflem  45984  fmtno4prmfac  46691  sfprmdvdsmersenne  46722  nnsum4primeseven  46919  nnsum4primesevenALTV  46920  bgoldbtbnd  46928