Theorem rexlimdv 3161

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  rexlimdva  3163  rexlimdva2  3165  rexlimdv3a  3167  rexlimdvw  3168  rexlimdvv  3218  rexlimdvvva  3220  elpwunsn  4641  onelssex  6412  eldmrexrnb  7093  weniso  7365  ssorduni  7794  onint  7805  limuni3  7864  peano5  7906  funcnvuni  7945  funeldmdif  8060  frxp  8141  fnwe2lem3  8150  smoiun  8373  tfrlem9  8397  oaordex  8570  oalimcl  8572  oaass  8573  findcard2  9184  findcard3  9278  frfi  9280  unblem1  9288  ordiso2  9513  inf3lem3  9635  r1sdom  9785  tz9.12lem3  9800  kardenOLD  9964  infxpenlem  10096  cardinfima  10180  iunfictbso  10197  dfac5  10211  cfcoflem  10354  fin23lem11  10399  fin23lem30  10424  fin1a2lem13  10494  axdc3lem2  10533  konigthlem  10657  fpwwe2lem11  10730  tskuni  10872  axgroth6  10917  nqereu  11018  genpnmax  11096  ltaddpr  11123  recexsrlem  11192  mulgt0sr  11194  axrrecex  11252  axpre-sup  11258  addrid  11494  addlid  11497  recex  11952  btwnz  12806  lbzbi  13067  qbtwnre  13333  caubnd  15532  divalglem9  16577  unbenlem  17092  firest  17609  imasmnd2  18974  imasgrp2  19271  pmtrfrn  19678  pgpfi  19825  sylow2blem3  19842  imasrng  20405  imasring  20566  lspsneq  21406  lspdisj  21409  elcls  23397  elcls3  23407  subbascn  23578  cmpsublem  23723  cmpsub  23724  nllyidm  23814  comppfsc  23857  ptpjopn  23937  fbfinnfr  24166  filin  24179  isfil2  24181  infil  24188  fgss2  24199  fgfil  24200  fgcl  24203  fgabs  24204  elfm2  24273  rnelfm  24278  fmfnfmlem2  24280  fmfnfmlem4  24282  fmco  24286  flffbas  24320  cnpflf2  24325  fclscf  24350  alexsubALTlem2  24373  alexsubALTlem3  24374  alexsubALTlem4  24375  alexsubALT  24376  neibl  24826  met2ndc  24848  metcnp3  24865  icccmplem2  25149  xrge0tsms  25160  fgcfil  25598  volfiniun  25874  dyadmax  25925  dyadmbllem  25926  c1liplem1  26322  dgrlem  26554  axcontlem10  29557  usgredg2vtxeuALT  29809  ushgredgedg  29816  ushgredgedgloop  29818  uhgrspan1  29890  nbuhgr2vtx1edgblem  29938  erclwwlksym  30618  erclwwlknsym  30667  umgr2cycllem  30752  umgr2cycl  30753  1pthon2v  30760  conngrv2edg  30802  lpni  31088  grpoidinvlem3  31114  grporcan  31126  omlsii  32011  spansncol  32176  spansnss  32179  spanunsni  32187  h1datomi  32189  nmopsetretALT  32471  branmfn  32713  chjatom  32965  cvbr4i  32975  atomli  32990  xrge0tsmsd  33681  sat1el2xp  36231  fmlasuc  36238  satffunlem1lem2  36255  satffunlem2lem1  36256  satffunlem2lem2  36258  dfon2lem6  36643  colineardim1  36919  finminlem  37199  nn0prpwlem  37203  neibastop2lem  37241  neibastop2  37242  fgmin  37251  exrecfnlem  38396  heiborlem10  38848  prtlem15  40026  lshpcmp  40139  lsatn0  40150  lsatcmp  40154  lsmsat  40159  lsatcv0  40182  l1cvpat  40205  eqlkr  40250  lshpkrlem1  40261  lshpkrlem6  40266  lfl1dim  40272  lfl1dim2N  40273  lkrss2N  40320  athgt  40607  3dim2  40619  llnle  40669  llncmp  40673  lplnle  40691  lplnnle2at  40692  llncvrlpln2  40708  llncvrlpln  40709  lplncmp  40713  lplnexllnN  40715  lvolnle3at  40733  lplncvrlvol2  40766  lplncvrlvol  40767  lvolcmp  40768  pointpsubN  40902  pclfinN  41051  pclfinclN  41101  osumcllem11N  41117  pexmidlem4N  41124  cdleme17d3  41647  cdlemeg46gfre  41683  cdleme48gfv1  41687  cdleme50trn2  41702  trlord  41720  cdlemg6e  41773  cdlemj3  41974  diaelrnN  42196  diaintclN  42209  dia2dimlem6  42220  cdlemm10N  42269  dibintclN  42318  dihord6apre  42407  dihord5b  42410  dihord5apre  42413  dihglblem5apreN  42442  dihglblem2N  42445  dihglblem3N  42446  dihglbcpreN  42451  dihintcl  42495  lclkrlem2y  42682  lcfrvalsnN  42692  isnacs3  43815  jm2.26  44103  hbtlem5  44224  dflim5  44425  uzwo4  46164  iunincfi  46203  restuni3  46227  disjinfi  46301  ssnnf1octb  46303  choicefi  46308  mapssbi  46320  unirnmapsn  46321  iunmapsn  46324  supxrgere  46439  supxrgelem  46443  suplesup  46445  infleinf  46477  suplesup2  46481  rexabslelem  46522  islptre  46725  limcperiod  46734  limclner  46755  limsupmnfuzlem  46830  limsupre3lem  46836  coskpi2  46970  cosknegpi  46973  icccncfext  46991  stoweidlem27  47131  stoweidlem59  47163  fourierdlem41  47252  fourierdlem42  47253  fourierdlem70  47280  fourierdlem71  47281  fourierdlem81  47291  fourierswlem  47334  qndenserrnopnlem  47401  subsaliuncl  47462  subsalsal  47463  sge0tsms  47484  sge0fsum  47491  sge0supre  47493  sge0sup  47495  sge0rnbnd  47497  sge0pnffigt  47500  sge0resrn  47508  sge0split  47513  sge0iunmptlemfi  47517  sge0rpcpnf  47525  sge0isum  47531  sge0xaddlem2  47538  sge0uzfsumgt  47548  sge0seq  47550  sge0reuz  47551  nnfoctbdjlem  47559  nnfoctbdj  47560  meadjiunlem  47569  meaiuninclem  47584  carageniuncllem2  47626  caratheodorylem2  47631  ovnsupge0  47661  ovncvrrp  47668  hoidmv1lelem3  47697  hoidmv1le  47698  hoidmvlelem1  47699  hoidmvlelem2  47700  hoidmvlelem3  47701  ovnhoilem2  47706  opnvonmbllem2  47737  ovnovollem3  47762  smfpimbor1lem1  47902  smfco  47906  smfpimcc  47912  smfinflem  47921  nprmmul3  48705  fmtno4prmfac  48751  sfprmdvdsmersenne  48782  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  bgoldbtbnd  49001  grimuhgr  49079  clnbgrgrim  49126  uspgrlimlem2  49181