Theorem rexlimdv 3162

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  rexlimdva  3164  rexlimdva2  3166  rexlimdv3a  3168  rexlimdvw  3169  rexlimdvv  3219  rexlimdvvva  3221  elpwunsn  4645  onelssex  6411  eldmrexrnb  7090  weniso  7362  ssorduni  7791  onint  7802  limuni3  7861  peano5  7903  funcnvuni  7942  funeldmdif  8057  frxp  8136  smoiun  8362  tfrlem9  8386  oaordex  8559  oalimcl  8561  oaass  8562  findcard2  9173  findcard3  9267  frfi  9269  unblem1  9277  ordiso2  9502  inf3lem3  9624  r1sdom  9774  tz9.12lem3  9789  kardenOLD  9953  infxpenlem  10085  cardinfima  10169  iunfictbso  10186  dfac5  10200  cfcoflem  10343  fin23lem11  10388  fin23lem30  10413  fin1a2lem13  10483  axdc3lem2  10522  konigthlem  10646  fpwwe2lem11  10719  tskuni  10861  axgroth6  10906  nqereu  11007  genpnmax  11085  ltaddpr  11112  recexsrlem  11181  mulgt0sr  11183  axrrecex  11241  axpre-sup  11247  addrid  11483  addlid  11486  recex  11941  btwnz  12795  lbzbi  13056  qbtwnre  13322  caubnd  15519  divalglem9  16564  unbenlem  17079  firest  17596  imasmnd2  18961  imasgrp2  19258  pmtrfrn  19665  pgpfi  19812  sylow2blem3  19829  imasrng  20392  imasring  20553  lspsneq  21393  lspdisj  21396  elcls  23384  elcls3  23394  subbascn  23565  cmpsublem  23710  cmpsub  23711  nllyidm  23801  comppfsc  23844  ptpjopn  23924  fbfinnfr  24153  filin  24166  isfil2  24168  infil  24175  fgss2  24186  fgfil  24187  fgcl  24190  fgabs  24191  elfm2  24260  rnelfm  24265  fmfnfmlem2  24267  fmfnfmlem4  24269  fmco  24273  flffbas  24307  cnpflf2  24312  fclscf  24337  alexsubALTlem2  24360  alexsubALTlem3  24361  alexsubALTlem4  24362  alexsubALT  24363  neibl  24813  met2ndc  24835  metcnp3  24852  icccmplem2  25136  xrge0tsms  25147  fgcfil  25585  volfiniun  25861  dyadmax  25912  dyadmbllem  25913  c1liplem1  26309  dgrlem  26541  axcontlem10  29544  usgredg2vtxeuALT  29796  ushgredgedg  29803  ushgredgedgloop  29805  uhgrspan1  29877  nbuhgr2vtx1edgblem  29925  erclwwlksym  30605  erclwwlknsym  30654  umgr2cycllem  30739  umgr2cycl  30740  1pthon2v  30747  conngrv2edg  30789  lpni  31075  grpoidinvlem3  31101  grporcan  31113  omlsii  31998  spansncol  32163  spansnss  32166  spanunsni  32174  h1datomi  32176  nmopsetretALT  32458  branmfn  32700  chjatom  32952  cvbr4i  32962  atomli  32977  xrge0tsmsd  33627  sat1el2xp  36123  fmlasuc  36130  satffunlem1lem2  36147  satffunlem2lem1  36148  satffunlem2lem2  36150  dfon2lem6  36530  colineardim1  36806  finminlem  37086  nn0prpwlem  37090  neibastop2lem  37128  neibastop2  37129  fgmin  37138  exrecfnlem  38282  heiborlem10  38734  prtlem15  39912  lshpcmp  40025  lsatn0  40036  lsatcmp  40040  lsmsat  40045  lsatcv0  40068  l1cvpat  40091  eqlkr  40136  lshpkrlem1  40147  lshpkrlem6  40152  lfl1dim  40158  lfl1dim2N  40159  lkrss2N  40206  athgt  40493  3dim2  40505  llnle  40555  llncmp  40559  lplnle  40577  lplnnle2at  40578  llncvrlpln2  40594  llncvrlpln  40595  lplncmp  40599  lplnexllnN  40601  lvolnle3at  40619  lplncvrlvol2  40652  lplncvrlvol  40653  lvolcmp  40654  pointpsubN  40788  pclfinN  40937  pclfinclN  40987  osumcllem11N  41003  pexmidlem4N  41010  cdleme17d3  41533  cdlemeg46gfre  41569  cdleme48gfv1  41573  cdleme50trn2  41588  trlord  41606  cdlemg6e  41659  cdlemj3  41860  diaelrnN  42082  diaintclN  42095  dia2dimlem6  42106  cdlemm10N  42155  dibintclN  42204  dihord6apre  42293  dihord5b  42296  dihord5apre  42299  dihglblem5apreN  42328  dihglblem2N  42331  dihglblem3N  42332  dihglbcpreN  42337  dihintcl  42381  lclkrlem2y  42568  lcfrvalsnN  42578  isnacs3  43700  jm2.26  43988  fnwe2lem2  44037  hbtlem5  44114  dflim5  44315  uzwo4  46039  iunincfi  46078  restuni3  46102  disjinfi  46176  ssnnf1octb  46178  choicefi  46183  mapssbi  46195  unirnmapsn  46196  iunmapsn  46199  supxrgere  46314  supxrgelem  46318  suplesup  46320  infleinf  46352  suplesup2  46356  rexabslelem  46397  islptre  46600  limcperiod  46609  limclner  46630  limsupmnfuzlem  46705  limsupre3lem  46711  coskpi2  46845  cosknegpi  46848  icccncfext  46866  stoweidlem27  47006  stoweidlem59  47038  fourierdlem41  47127  fourierdlem42  47128  fourierdlem70  47155  fourierdlem71  47156  fourierdlem81  47166  fourierswlem  47209  qndenserrnopnlem  47276  subsaliuncl  47337  subsalsal  47338  sge0tsms  47359  sge0fsum  47366  sge0supre  47368  sge0sup  47370  sge0rnbnd  47372  sge0pnffigt  47375  sge0resrn  47383  sge0split  47388  sge0iunmptlemfi  47392  sge0rpcpnf  47400  sge0isum  47406  sge0xaddlem2  47413  sge0uzfsumgt  47423  sge0seq  47425  sge0reuz  47426  nnfoctbdjlem  47434  nnfoctbdj  47435  meadjiunlem  47444  meaiuninclem  47459  carageniuncllem2  47501  caratheodorylem2  47506  ovnsupge0  47536  ovncvrrp  47543  hoidmv1lelem3  47572  hoidmv1le  47573  hoidmvlelem1  47574  hoidmvlelem2  47575  hoidmvlelem3  47576  ovnhoilem2  47581  opnvonmbllem2  47612  ovnovollem3  47637  smfpimbor1lem1  47777  smfco  47781  smfpimcc  47787  smfinflem  47796  nprmmul3  48580  fmtno4prmfac  48626  sfprmdvdsmersenne  48657  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  bgoldbtbnd  48876  grimuhgr  48954  clnbgrgrim  49001  uspgrlimlem2  49056