Theorem rexlimdv 3242

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  rexlimdva  3243  rexlimdv3a  3245  rexlimdva2  3246  rexlimdvw  3249  rexlimdvv  3252  elpwunsn  4581  eldmrexrnb  6835  weniso  7086  ssorduni  7480  onint  7490  limuni3  7547  funcnvuni  7618  funeldmdif  7729  frxp  7803  smoiun  7981  tfrlem9  8004  oaordex  8167  oalimcl  8169  oaass  8170  findcard3  8745  frfi  8747  unblem1  8754  ordiso2  8963  inf3lem3  9077  r1sdom  9187  tz9.12lem3  9202  karden  9308  infxpenlem  9424  cardinfima  9508  iunfictbso  9525  dfac5  9539  cfcoflem  9683  fin23lem11  9728  fin23lem30  9753  fin1a2lem13  9823  axdc3lem2  9862  konigthlem  9979  fpwwe2lem12  10052  tskuni  10194  axgroth6  10239  nqereu  10340  genpnmax  10418  ltaddpr  10445  recexsrlem  10514  mulgt0sr  10516  axrrecex  10574  axpre-sup  10580  addid1  10809  addid2  10812  recex  11261  btwnz  12072  lbzbi  12324  qbtwnre  12580  caubnd  14710  divalglem9  15742  unbenlem  16234  firest  16698  imasmnd2  17940  imasgrp2  18206  pmtrfrn  18578  pgpfi  18722  sylow2blem3  18739  imasring  19365  lspsneq  19887  lspdisj  19890  elcls  21678  elcls3  21688  subbascn  21859  cmpsublem  22004  cmpsub  22005  nllyidm  22094  comppfsc  22137  ptpjopn  22217  fbfinnfr  22446  filin  22459  isfil2  22461  infil  22468  fgss2  22479  fgfil  22480  fgcl  22483  fgabs  22484  elfm2  22553  rnelfm  22558  fmfnfmlem2  22560  fmfnfmlem4  22562  fmco  22566  flffbas  22600  cnpflf2  22605  fclscf  22630  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALTlem4  22655  alexsubALT  22656  neibl  23108  met2ndc  23130  metcnp3  23147  icccmplem2  23428  xrge0tsms  23439  fgcfil  23875  volfiniun  24151  dyadmax  24202  dyadmbllem  24203  c1liplem1  24599  dgrlem  24826  axcontlem10  26767  usgredg2vtxeuALT  27012  ushgredgedg  27019  ushgredgedgloop  27021  uhgrspan1  27093  nbuhgr2vtx1edgblem  27141  erclwwlksym  27806  erclwwlknsym  27855  1pthon2v  27938  conngrv2edg  27980  lpni  28263  grpoidinvlem3  28289  grporcan  28301  omlsii  29186  spansncol  29351  spansnss  29354  spanunsni  29362  h1datomi  29364  nmopsetretALT  29646  branmfn  29888  chjatom  30140  cvbr4i  30150  atomli  30165  xrge0tsmsd  30742  umgr2cycllem  32500  umgr2cycl  32501  sat1el2xp  32739  fmlasuc  32746  satffunlem1lem2  32763  satffunlem2lem1  32764  satffunlem2lem2  32766  dfon2lem6  33146  trpredrec  33190  colineardim1  33635  finminlem  33779  nn0prpwlem  33783  neibastop2lem  33821  neibastop2  33822  fgmin  33831  exrecfnlem  34796  heiborlem10  35258  prtlem15  36171  lshpcmp  36284  lsatn0  36295  lsatcmp  36299  lsmsat  36304  lsatcv0  36327  l1cvpat  36350  eqlkr  36395  lshpkrlem1  36406  lshpkrlem6  36411  lfl1dim  36417  lfl1dim2N  36418  lkrss2N  36465  athgt  36752  3dim2  36764  llnle  36814  llncmp  36818  lplnle  36836  lplnnle2at  36837  llncvrlpln2  36853  llncvrlpln  36854  lplncmp  36858  lplnexllnN  36860  lvolnle3at  36878  lplncvrlvol2  36911  lplncvrlvol  36912  lvolcmp  36913  pointpsubN  37047  pclfinN  37196  pclfinclN  37246  osumcllem11N  37262  pexmidlem4N  37269  cdleme17d3  37792  cdlemeg46gfre  37828  cdleme48gfv1  37832  cdleme50trn2  37847  trlord  37865  cdlemg6e  37918  cdlemj3  38119  diaelrnN  38341  diaintclN  38354  dia2dimlem6  38365  cdlemm10N  38414  dibintclN  38463  dihord6apre  38552  dihord5b  38555  dihord5apre  38558  dihglblem5apreN  38587  dihglblem2N  38590  dihglblem3N  38591  dihglbcpreN  38596  dihintcl  38640  lclkrlem2y  38827  lcfrvalsnN  38837  isnacs3  39651  jm2.26  39943  fnwe2lem2  39995  hbtlem5  40072  uzwo4  41687  iunincfi  41730  restuni3  41753  disjinfi  41820  ssnnf1octb  41822  choicefi  41829  mapssbi  41842  unirnmapsn  41843  ssmapsn  41845  iunmapsn  41846  supxrgere  41965  supxrgelem  41969  suplesup  41971  infleinf  42004  suplesup2  42008  rexabslelem  42055  islptre  42261  limcperiod  42270  limclner  42293  limsupmnfuzlem  42368  limsupre3lem  42374  coskpi2  42508  cosknegpi  42511  icccncfext  42529  stoweidlem27  42669  stoweidlem59  42701  fourierdlem41  42790  fourierdlem42  42791  fourierdlem70  42818  fourierdlem71  42819  fourierdlem81  42829  fourierswlem  42872  qndenserrnopnlem  42939  subsaliuncl  42998  subsalsal  42999  sge0tsms  43019  sge0fsum  43026  sge0supre  43028  sge0sup  43030  sge0rnbnd  43032  sge0pnffigt  43035  sge0resrn  43043  sge0split  43048  sge0iunmptlemfi  43052  sge0rpcpnf  43060  sge0isum  43066  sge0xaddlem2  43073  sge0uzfsumgt  43083  sge0seq  43085  sge0reuz  43086  nnfoctbdjlem  43094  nnfoctbdj  43095  meadjiunlem  43104  meaiuninclem  43119  carageniuncllem2  43161  caratheodorylem2  43166  ovnsupge0  43196  ovncvrrp  43203  hoidmv1lelem3  43232  hoidmv1le  43233  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  ovnhoilem2  43241  opnvonmbllem2  43272  ovolval5lem3  43293  ovnovollem3  43297  sssmf  43372  smfpimbor1lem1  43430  smfco  43434  smfpimcc  43439  smfinflem  43448  fmtno4prmfac  44089  sfprmdvdsmersenne  44121  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbnd  44327