Theorem rexlimdv 3150

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  rexlimdva  3152  rexlimdva2  3154  rexlimdv3a  3156  rexlimdvw  3157  rexlimdvv  3209  rexlimdvvva  3211  elpwunsn  4688  onelssex  6433  eldmrexrnb  7111  weniso  7373  ssorduni  7797  onint  7809  limuni3  7872  peano5  7915  funcnvuni  7954  funeldmdif  8071  frxp  8149  smoiun  8399  tfrlem9  8423  oaordex  8594  oalimcl  8596  oaass  8597  findcard2  9202  findcard3  9315  findcard3OLD  9316  frfi  9318  unblem1  9325  ordiso2  9552  inf3lem3  9667  r1sdom  9811  tz9.12lem3  9826  karden  9932  infxpenlem  10050  cardinfima  10134  iunfictbso  10151  dfac5  10166  cfcoflem  10309  fin23lem11  10354  fin23lem30  10379  fin1a2lem13  10449  axdc3lem2  10488  konigthlem  10605  fpwwe2lem11  10678  tskuni  10820  axgroth6  10865  nqereu  10966  genpnmax  11044  ltaddpr  11071  recexsrlem  11140  mulgt0sr  11142  axrrecex  11200  axpre-sup  11206  addrid  11438  addlid  11441  recex  11892  btwnz  12718  lbzbi  12975  qbtwnre  13237  caubnd  15393  divalglem9  16434  unbenlem  16941  firest  17478  imasmnd2  18799  imasgrp2  19085  pmtrfrn  19490  pgpfi  19637  sylow2blem3  19654  imasrng  20194  imasring  20343  lspsneq  21141  lspdisj  21144  elcls  23096  elcls3  23106  subbascn  23277  cmpsublem  23422  cmpsub  23423  nllyidm  23512  comppfsc  23555  ptpjopn  23635  fbfinnfr  23864  filin  23877  isfil2  23879  infil  23886  fgss2  23897  fgfil  23898  fgcl  23901  fgabs  23902  elfm2  23971  rnelfm  23976  fmfnfmlem2  23978  fmfnfmlem4  23980  fmco  23984  flffbas  24018  cnpflf2  24023  fclscf  24048  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  alexsubALT  24074  neibl  24529  met2ndc  24551  metcnp3  24568  icccmplem2  24858  xrge0tsms  24869  fgcfil  25318  volfiniun  25595  dyadmax  25646  dyadmbllem  25647  c1liplem1  26049  dgrlem  26282  axcontlem10  29002  usgredg2vtxeuALT  29253  ushgredgedg  29260  ushgredgedgloop  29262  uhgrspan1  29334  nbuhgr2vtx1edgblem  29382  erclwwlksym  30049  erclwwlknsym  30098  1pthon2v  30181  conngrv2edg  30223  lpni  30508  grpoidinvlem3  30534  grporcan  30546  omlsii  31431  spansncol  31596  spansnss  31599  spanunsni  31607  h1datomi  31609  nmopsetretALT  31891  branmfn  32133  chjatom  32385  cvbr4i  32395  atomli  32410  xrge0tsmsd  33047  umgr2cycllem  35124  umgr2cycl  35125  sat1el2xp  35363  fmlasuc  35370  satffunlem1lem2  35387  satffunlem2lem1  35388  satffunlem2lem2  35390  dfon2lem6  35769  colineardim1  36042  finminlem  36300  nn0prpwlem  36304  neibastop2lem  36342  neibastop2  36343  fgmin  36352  exrecfnlem  37361  heiborlem10  37806  prtlem15  38856  lshpcmp  38969  lsatn0  38980  lsatcmp  38984  lsmsat  38989  lsatcv0  39012  l1cvpat  39035  eqlkr  39080  lshpkrlem1  39091  lshpkrlem6  39096  lfl1dim  39102  lfl1dim2N  39103  lkrss2N  39150  athgt  39438  3dim2  39450  llnle  39500  llncmp  39504  lplnle  39522  lplnnle2at  39523  llncvrlpln2  39539  llncvrlpln  39540  lplncmp  39544  lplnexllnN  39546  lvolnle3at  39564  lplncvrlvol2  39597  lplncvrlvol  39598  lvolcmp  39599  pointpsubN  39733  pclfinN  39882  pclfinclN  39932  osumcllem11N  39948  pexmidlem4N  39955  cdleme17d3  40478  cdlemeg46gfre  40514  cdleme48gfv1  40518  cdleme50trn2  40533  trlord  40551  cdlemg6e  40604  cdlemj3  40805  diaelrnN  41027  diaintclN  41040  dia2dimlem6  41051  cdlemm10N  41100  dibintclN  41149  dihord6apre  41238  dihord5b  41241  dihord5apre  41244  dihglblem5apreN  41273  dihglblem2N  41276  dihglblem3N  41277  dihglbcpreN  41282  dihintcl  41326  lclkrlem2y  41513  lcfrvalsnN  41523  isnacs3  42697  jm2.26  42990  fnwe2lem2  43039  hbtlem5  43116  dflim5  43318  uzwo4  44992  iunincfi  45033  restuni3  45057  disjinfi  45134  ssnnf1octb  45136  choicefi  45142  mapssbi  45155  unirnmapsn  45156  iunmapsn  45159  supxrgere  45282  supxrgelem  45286  suplesup  45288  infleinf  45321  suplesup2  45325  rexabslelem  45367  islptre  45574  limcperiod  45583  limclner  45606  limsupmnfuzlem  45681  limsupre3lem  45687  coskpi2  45821  cosknegpi  45824  icccncfext  45842  stoweidlem27  45982  stoweidlem59  46014  fourierdlem41  46103  fourierdlem42  46104  fourierdlem70  46131  fourierdlem71  46132  fourierdlem81  46142  fourierswlem  46185  qndenserrnopnlem  46252  subsaliuncl  46313  subsalsal  46314  sge0tsms  46335  sge0fsum  46342  sge0supre  46344  sge0sup  46346  sge0rnbnd  46348  sge0pnffigt  46351  sge0resrn  46359  sge0split  46364  sge0iunmptlemfi  46368  sge0rpcpnf  46376  sge0isum  46382  sge0xaddlem2  46389  sge0uzfsumgt  46399  sge0seq  46401  sge0reuz  46402  nnfoctbdjlem  46410  nnfoctbdj  46411  meadjiunlem  46420  meaiuninclem  46435  carageniuncllem2  46477  caratheodorylem2  46482  ovnsupge0  46512  ovncvrrp  46519  hoidmv1lelem3  46548  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnhoilem2  46557  opnvonmbllem2  46588  ovnovollem3  46613  sssmf  46693  smfpimbor1lem1  46753  smfco  46757  smfpimcc  46763  smfinflem  46772  fmtno4prmfac  47496  sfprmdvdsmersenne  47527  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbtbnd  47733  grimuhgr  47815  clnbgrgrim  47839  uspgrlimlem2  47891