Theorem rexlimdv 3133

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  rexlimdva  3135  rexlimdva2  3137  rexlimdv3a  3139  rexlimdvw  3140  rexlimdvv  3194  rexlimdvvva  3196  elpwunsn  4651  onelssex  6384  eldmrexrnb  7067  weniso  7332  ssorduni  7758  onint  7769  limuni3  7831  peano5  7872  funcnvuni  7911  funeldmdif  8030  frxp  8108  smoiun  8333  tfrlem9  8356  oaordex  8525  oalimcl  8527  oaass  8528  findcard2  9134  findcard3  9236  findcard3OLD  9237  frfi  9239  unblem1  9246  ordiso2  9475  inf3lem3  9590  r1sdom  9734  tz9.12lem3  9749  karden  9855  infxpenlem  9973  cardinfima  10057  iunfictbso  10074  dfac5  10089  cfcoflem  10232  fin23lem11  10277  fin23lem30  10302  fin1a2lem13  10372  axdc3lem2  10411  konigthlem  10528  fpwwe2lem11  10601  tskuni  10743  axgroth6  10788  nqereu  10889  genpnmax  10967  ltaddpr  10994  recexsrlem  11063  mulgt0sr  11065  axrrecex  11123  axpre-sup  11129  addrid  11361  addlid  11364  recex  11817  btwnz  12644  lbzbi  12902  qbtwnre  13166  caubnd  15332  divalglem9  16378  unbenlem  16886  firest  17402  imasmnd2  18708  imasgrp2  18994  pmtrfrn  19395  pgpfi  19542  sylow2blem3  19559  imasrng  20093  imasring  20246  lspsneq  21039  lspdisj  21042  elcls  22967  elcls3  22977  subbascn  23148  cmpsublem  23293  cmpsub  23294  nllyidm  23383  comppfsc  23426  ptpjopn  23506  fbfinnfr  23735  filin  23748  isfil2  23750  infil  23757  fgss2  23768  fgfil  23769  fgcl  23772  fgabs  23773  elfm2  23842  rnelfm  23847  fmfnfmlem2  23849  fmfnfmlem4  23851  fmco  23855  flffbas  23889  cnpflf2  23894  fclscf  23919  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  alexsubALT  23945  neibl  24396  met2ndc  24418  metcnp3  24435  icccmplem2  24719  xrge0tsms  24730  fgcfil  25178  volfiniun  25455  dyadmax  25506  dyadmbllem  25507  c1liplem1  25908  dgrlem  26141  axcontlem10  28907  usgredg2vtxeuALT  29156  ushgredgedg  29163  ushgredgedgloop  29165  uhgrspan1  29237  nbuhgr2vtx1edgblem  29285  erclwwlksym  29957  erclwwlknsym  30006  1pthon2v  30089  conngrv2edg  30131  lpni  30416  grpoidinvlem3  30442  grporcan  30454  omlsii  31339  spansncol  31504  spansnss  31507  spanunsni  31515  h1datomi  31517  nmopsetretALT  31799  branmfn  32041  chjatom  32293  cvbr4i  32303  atomli  32318  xrge0tsmsd  33009  umgr2cycllem  35134  umgr2cycl  35135  sat1el2xp  35373  fmlasuc  35380  satffunlem1lem2  35397  satffunlem2lem1  35398  satffunlem2lem2  35400  dfon2lem6  35783  colineardim1  36056  finminlem  36313  nn0prpwlem  36317  neibastop2lem  36355  neibastop2  36356  fgmin  36365  exrecfnlem  37374  heiborlem10  37821  prtlem15  38875  lshpcmp  38988  lsatn0  38999  lsatcmp  39003  lsmsat  39008  lsatcv0  39031  l1cvpat  39054  eqlkr  39099  lshpkrlem1  39110  lshpkrlem6  39115  lfl1dim  39121  lfl1dim2N  39122  lkrss2N  39169  athgt  39457  3dim2  39469  llnle  39519  llncmp  39523  lplnle  39541  lplnnle2at  39542  llncvrlpln2  39558  llncvrlpln  39559  lplncmp  39563  lplnexllnN  39565  lvolnle3at  39583  lplncvrlvol2  39616  lplncvrlvol  39617  lvolcmp  39618  pointpsubN  39752  pclfinN  39901  pclfinclN  39951  osumcllem11N  39967  pexmidlem4N  39974  cdleme17d3  40497  cdlemeg46gfre  40533  cdleme48gfv1  40537  cdleme50trn2  40552  trlord  40570  cdlemg6e  40623  cdlemj3  40824  diaelrnN  41046  diaintclN  41059  dia2dimlem6  41070  cdlemm10N  41119  dibintclN  41168  dihord6apre  41257  dihord5b  41260  dihord5apre  41263  dihglblem5apreN  41292  dihglblem2N  41295  dihglblem3N  41296  dihglbcpreN  41301  dihintcl  41345  lclkrlem2y  41532  lcfrvalsnN  41542  isnacs3  42705  jm2.26  42998  fnwe2lem2  43047  hbtlem5  43124  dflim5  43325  uzwo4  45054  iunincfi  45095  restuni3  45119  disjinfi  45193  ssnnf1octb  45195  choicefi  45201  mapssbi  45214  unirnmapsn  45215  iunmapsn  45218  supxrgere  45336  supxrgelem  45340  suplesup  45342  infleinf  45375  suplesup2  45379  rexabslelem  45421  islptre  45624  limcperiod  45633  limclner  45656  limsupmnfuzlem  45731  limsupre3lem  45737  coskpi2  45871  cosknegpi  45874  icccncfext  45892  stoweidlem27  46032  stoweidlem59  46064  fourierdlem41  46153  fourierdlem42  46154  fourierdlem70  46181  fourierdlem71  46182  fourierdlem81  46192  fourierswlem  46235  qndenserrnopnlem  46302  subsaliuncl  46363  subsalsal  46364  sge0tsms  46385  sge0fsum  46392  sge0supre  46394  sge0sup  46396  sge0rnbnd  46398  sge0pnffigt  46401  sge0resrn  46409  sge0split  46414  sge0iunmptlemfi  46418  sge0rpcpnf  46426  sge0isum  46432  sge0xaddlem2  46439  sge0uzfsumgt  46449  sge0seq  46451  sge0reuz  46452  nnfoctbdjlem  46460  nnfoctbdj  46461  meadjiunlem  46470  meaiuninclem  46485  carageniuncllem2  46527  caratheodorylem2  46532  ovnsupge0  46562  ovncvrrp  46569  hoidmv1lelem3  46598  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  ovnhoilem2  46607  opnvonmbllem2  46638  ovnovollem3  46663  sssmf  46743  smfpimbor1lem1  46803  smfco  46807  smfpimcc  46813  smfinflem  46822  fmtno4prmfac  47577  sfprmdvdsmersenne  47608  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  bgoldbtbnd  47814  grimuhgr  47891  clnbgrgrim  47938  uspgrlimlem2  47992