Theorem rexlimdv 3212

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  rexlimdva  3213  rexlimdv3a  3215  rexlimdva2  3216  rexlimdvw  3219  rexlimdvv  3222  elpwunsn  4619  eldmrexrnb  6968  weniso  7225  ssorduni  7629  onint  7640  limuni3  7699  peano5  7740  funcnvuni  7778  funeldmdif  7889  frxp  7967  smoiun  8192  tfrlem9  8216  oaordex  8389  oalimcl  8391  oaass  8392  findcard2  8947  findcard3  9057  frfi  9059  unblem1  9066  ordiso2  9274  inf3lem3  9388  r1sdom  9532  tz9.12lem3  9547  karden  9653  infxpenlem  9769  cardinfima  9853  iunfictbso  9870  dfac5  9884  cfcoflem  10028  fin23lem11  10073  fin23lem30  10098  fin1a2lem13  10168  axdc3lem2  10207  konigthlem  10324  fpwwe2lem11  10397  tskuni  10539  axgroth6  10584  nqereu  10685  genpnmax  10763  ltaddpr  10790  recexsrlem  10859  mulgt0sr  10861  axrrecex  10919  axpre-sup  10925  addid1  11155  addid2  11158  recex  11607  btwnz  12423  lbzbi  12676  qbtwnre  12933  caubnd  15070  divalglem9  16110  unbenlem  16609  firest  17143  imasmnd2  18422  imasgrp2  18690  pmtrfrn  19066  pgpfi  19210  sylow2blem3  19227  imasring  19858  lspsneq  20384  lspdisj  20387  elcls  22224  elcls3  22234  subbascn  22405  cmpsublem  22550  cmpsub  22551  nllyidm  22640  comppfsc  22683  ptpjopn  22763  fbfinnfr  22992  filin  23005  isfil2  23007  infil  23014  fgss2  23025  fgfil  23026  fgcl  23029  fgabs  23030  elfm2  23099  rnelfm  23104  fmfnfmlem2  23106  fmfnfmlem4  23108  fmco  23112  flffbas  23146  cnpflf2  23151  fclscf  23176  alexsubALTlem2  23199  alexsubALTlem3  23200  alexsubALTlem4  23201  alexsubALT  23202  neibl  23657  met2ndc  23679  metcnp3  23696  icccmplem2  23986  xrge0tsms  23997  fgcfil  24435  volfiniun  24711  dyadmax  24762  dyadmbllem  24763  c1liplem1  25160  dgrlem  25390  axcontlem10  27341  usgredg2vtxeuALT  27589  ushgredgedg  27596  ushgredgedgloop  27598  uhgrspan1  27670  nbuhgr2vtx1edgblem  27718  erclwwlksym  28385  erclwwlknsym  28434  1pthon2v  28517  conngrv2edg  28559  lpni  28842  grpoidinvlem3  28868  grporcan  28880  omlsii  29765  spansncol  29930  spansnss  29933  spanunsni  29941  h1datomi  29943  nmopsetretALT  30225  branmfn  30467  chjatom  30719  cvbr4i  30729  atomli  30744  xrge0tsmsd  31317  umgr2cycllem  33102  umgr2cycl  33103  sat1el2xp  33341  fmlasuc  33348  satffunlem1lem2  33365  satffunlem2lem1  33366  satffunlem2lem2  33368  onelssex  33661  dfon2lem6  33764  colineardim1  34363  finminlem  34507  nn0prpwlem  34511  neibastop2lem  34549  neibastop2  34550  fgmin  34559  exrecfnlem  35550  heiborlem10  35978  prtlem15  36889  lshpcmp  37002  lsatn0  37013  lsatcmp  37017  lsmsat  37022  lsatcv0  37045  l1cvpat  37068  eqlkr  37113  lshpkrlem1  37124  lshpkrlem6  37129  lfl1dim  37135  lfl1dim2N  37136  lkrss2N  37183  athgt  37470  3dim2  37482  llnle  37532  llncmp  37536  lplnle  37554  lplnnle2at  37555  llncvrlpln2  37571  llncvrlpln  37572  lplncmp  37576  lplnexllnN  37578  lvolnle3at  37596  lplncvrlvol2  37629  lplncvrlvol  37630  lvolcmp  37631  pointpsubN  37765  pclfinN  37914  pclfinclN  37964  osumcllem11N  37980  pexmidlem4N  37987  cdleme17d3  38510  cdlemeg46gfre  38546  cdleme48gfv1  38550  cdleme50trn2  38565  trlord  38583  cdlemg6e  38636  cdlemj3  38837  diaelrnN  39059  diaintclN  39072  dia2dimlem6  39083  cdlemm10N  39132  dibintclN  39181  dihord6apre  39270  dihord5b  39273  dihord5apre  39276  dihglblem5apreN  39305  dihglblem2N  39308  dihglblem3N  39309  dihglbcpreN  39314  dihintcl  39358  lclkrlem2y  39545  lcfrvalsnN  39555  isnacs3  40532  jm2.26  40824  fnwe2lem2  40876  hbtlem5  40953  uzwo4  42601  iunincfi  42644  restuni3  42667  disjinfi  42731  ssnnf1octb  42733  choicefi  42740  mapssbi  42753  unirnmapsn  42754  ssmapsn  42756  iunmapsn  42757  supxrgere  42872  supxrgelem  42876  suplesup  42878  infleinf  42911  suplesup2  42915  rexabslelem  42958  islptre  43160  limcperiod  43169  limclner  43192  limsupmnfuzlem  43267  limsupre3lem  43273  coskpi2  43407  cosknegpi  43410  icccncfext  43428  stoweidlem27  43568  stoweidlem59  43600  fourierdlem41  43689  fourierdlem42  43690  fourierdlem70  43717  fourierdlem71  43718  fourierdlem81  43728  fourierswlem  43771  qndenserrnopnlem  43838  subsaliuncl  43897  subsalsal  43898  sge0tsms  43918  sge0fsum  43925  sge0supre  43927  sge0sup  43929  sge0rnbnd  43931  sge0pnffigt  43934  sge0resrn  43942  sge0split  43947  sge0iunmptlemfi  43951  sge0rpcpnf  43959  sge0isum  43965  sge0xaddlem2  43972  sge0uzfsumgt  43982  sge0seq  43984  sge0reuz  43985  nnfoctbdjlem  43993  nnfoctbdj  43994  meadjiunlem  44003  meaiuninclem  44018  carageniuncllem2  44060  caratheodorylem2  44065  ovnsupge0  44095  ovncvrrp  44102  hoidmv1lelem3  44131  hoidmv1le  44132  hoidmvlelem1  44133  hoidmvlelem2  44134  hoidmvlelem3  44135  ovnhoilem2  44140  opnvonmbllem2  44171  ovolval5lem3  44192  ovnovollem3  44196  sssmf  44274  smfpimbor1lem1  44332  smfco  44336  smfpimcc  44341  smfinflem  44350  fmtno4prmfac  45024  sfprmdvdsmersenne  45055  nnsum4primeseven  45252  nnsum4primesevenALTV  45253  bgoldbtbnd  45261