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 2107  ∃wrex 3091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-ral 3095  df-rex 3096

This theorem is referenced by:  rexlimdva  3213  rexlimdv3a  3215  rexlimdva2  3216  rexlimdvw  3217  rexlimdvv  3220  elpwunsn  4452  eldmrexrnb  6632  weniso  6878  ssorduni  7265  onint  7275  limuni3  7332  funcnvuni  7400  frxp  7570  smoiun  7743  tfrlem9  7766  oaordex  7924  oalimcl  7926  oaass  7927  findcard3  8493  frfi  8495  unblem1  8502  ordiso2  8711  inf3lem3  8826  r1sdom  8936  tz9.12lem3  8951  karden  9057  infxpenlem  9171  cardinfima  9255  iunfictbso  9272  dfac5  9286  cfcoflem  9431  fin23lem11  9476  fin23lem30  9501  fin1a2lem13  9571  axdc3lem2  9610  konigthlem  9727  fpwwe2lem12  9800  tskuni  9942  axgroth6  9987  nqereu  10088  genpnmax  10166  ltaddpr  10193  recexsrlem  10262  mulgt0sr  10264  axrrecex  10322  axpre-sup  10328  addid1  10558  addid2  10561  recex  11009  btwnz  11835  lbzbi  12087  qbtwnre  12346  caubnd  14509  divalglem9  15535  unbenlem  16020  firest  16483  imasmnd2  17717  imasgrp2  17921  pmtrfrn  18265  pgpfi  18408  sylow2blem3  18425  imasring  19010  lspsneq  19521  lspdisj  19524  elcls  21289  elcls3  21299  subbascn  21470  cmpsublem  21615  cmpsub  21616  nllyidm  21705  comppfsc  21748  ptpjopn  21828  fbfinnfr  22057  filin  22070  isfil2  22072  infil  22079  fgss2  22090  fgfil  22091  fgcl  22094  fgabs  22095  elfm2  22164  rnelfm  22169  fmfnfmlem2  22171  fmfnfmlem4  22173  fmco  22177  flffbas  22211  cnpflf2  22216  fclscf  22241  alexsubALTlem2  22264  alexsubALTlem3  22265  alexsubALTlem4  22266  alexsubALT  22267  neibl  22718  met2ndc  22740  metcnp3  22757  icccmplem2  23038  xrge0tsms  23049  fgcfil  23481  volfiniun  23755  dyadmax  23806  dyadmbllem  23807  c1liplem1  24200  dgrlem  24426  axcontlem10  26326  usgredg2vtxeuALT  26572  ushgredgedg  26579  ushgredgedgloop  26581  ushgredgedgloopOLD  26582  uhgrspan1  26654  nbuhgr2vtx1edgblem  26702  erclwwlksym  27414  erclwwlknsym  27472  1pthon2v  27560  conngrv2edg  27602  lpni  27911  grpoidinvlem3  27937  grporcan  27949  omlsii  28838  spansncol  29003  spansnss  29006  spanunsni  29014  h1datomi  29016  nmopsetretALT  29298  branmfn  29540  chjatom  29792  cvbr4i  29802  atomli  29817  xrge0tsmsd  30351  dfon2lem6  32285  trpredrec  32330  colineardim1  32761  finminlem  32905  nn0prpwlem  32909  neibastop2lem  32947  neibastop2  32948  fgmin  32957  heiborlem10  34248  prtlem15  35034  lshpcmp  35147  lsatn0  35158  lsatcmp  35162  lsmsat  35167  lsatcv0  35190  l1cvpat  35213  eqlkr  35258  lshpkrlem1  35269  lshpkrlem6  35274  lfl1dim  35280  lfl1dim2N  35281  lkrss2N  35328  athgt  35615  3dim2  35627  llnle  35677  llncmp  35681  lplnle  35699  lplnnle2at  35700  llncvrlpln2  35716  llncvrlpln  35717  lplncmp  35721  lplnexllnN  35723  lvolnle3at  35741  lplncvrlvol2  35774  lplncvrlvol  35775  lvolcmp  35776  pointpsubN  35910  pclfinN  36059  pclfinclN  36109  osumcllem11N  36125  pexmidlem4N  36132  cdleme17d3  36655  cdlemeg46gfre  36691  cdleme48gfv1  36695  cdleme50trn2  36710  trlord  36728  cdlemg6e  36781  cdlemj3  36982  diaelrnN  37204  diaintclN  37217  dia2dimlem6  37228  cdlemm10N  37277  dibintclN  37326  dihord6apre  37415  dihord5b  37418  dihord5apre  37421  dihglblem5apreN  37450  dihglblem2N  37453  dihglblem3N  37454  dihglbcpreN  37459  dihintcl  37503  lclkrlem2y  37690  lcfrvalsnN  37700  isnacs3  38243  jm2.26  38538  fnwe2lem2  38590  hbtlem5  38667  uzwo4  40162  iunincfi  40213  restuni3  40240  disjinfi  40313  ssnnf1octb  40315  choicefi  40323  mapssbi  40336  unirnmapsn  40337  ssmapsn  40339  iunmapsn  40340  supxrgere  40467  supxrgelem  40471  suplesup  40473  infleinf  40506  suplesup2  40510  rexabslelem  40561  islptre  40769  limcperiod  40778  limclner  40801  limsupmnfuzlem  40876  limsupre3lem  40882  coskpi2  41015  cosknegpi  41018  icccncfext  41038  stoweidlem27  41181  stoweidlem59  41213  fourierdlem41  41302  fourierdlem42  41303  fourierdlem70  41330  fourierdlem71  41331  fourierdlem81  41341  fourierswlem  41384  qndenserrnopnlem  41451  subsaliuncl  41510  subsalsal  41511  sge0tsms  41531  sge0fsum  41538  sge0supre  41540  sge0sup  41542  sge0rnbnd  41544  sge0pnffigt  41547  sge0resrn  41555  sge0split  41560  sge0iunmptlemfi  41564  sge0rpcpnf  41572  sge0isum  41578  sge0xaddlem2  41585  sge0uzfsumgt  41595  sge0seq  41597  sge0reuz  41598  nnfoctbdjlem  41606  nnfoctbdj  41607  meadjiunlem  41616  meaiuninclem  41631  carageniuncllem2  41673  caratheodorylem2  41678  ovnsupge0  41708  ovncvrrp  41715  hoidmv1lelem3  41744  hoidmv1le  41745  hoidmvlelem1  41746  hoidmvlelem2  41747  hoidmvlelem3  41748  ovnhoilem2  41753  opnvonmbllem2  41784  ovolval5lem3  41805  ovnovollem3  41809  sssmf  41884  smfpimbor1lem1  41942  smfco  41946  smfpimcc  41951  smfinflem  41960  fmtno4prmfac  42515  sfprmdvdsmersenne  42551  nnsum4primeseven  42723  nnsum4primesevenALTV  42724  bgoldbtbnd  42732