Theorem rexlimdv 3165

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∃wrex 3090

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 1945

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

This theorem is used by:  rexlimdva  3167  rexlimdva2  3169  rexlimdv3a  3171  rexlimdvw  3172  rexlimdvv  3222  rexlimdvvva  3224  elpwunsn  4646  onelssex  6438  eldmrexrnb  7124  weniso  7395  ssorduni  7827  onint  7838  limuni3  7897  peano5  7939  funcnvuni  7978  funeldmdif  8094  frxp  8175  fnwe2lem3  8184  smoiun  8407  tfrlem9  8431  oaordex  8604  oalimcl  8606  oaass  8607  findcard2  9218  findcard3  9312  frfi  9314  unblem1  9322  ordiso2  9546  inf3lem3  9668  r1sdom  9818  tz9.12lem3  9833  kardenOLD  9997  infxpenlem  10131  cardinfima  10215  iunfictbso  10232  dfac5  10246  cfcoflem  10389  fin23lem11  10434  fin23lem30  10459  fin1a2lem13  10529  axdc3lem2  10568  konigthlem  10692  fpwwe2lem11  10765  tskuni  10907  axgroth6  10952  nqereu  11053  genpnmax  11131  ltaddpr  11158  recexsrlem  11227  mulgt0sr  11229  axrrecex  11287  axpre-sup  11293  addrid  11529  addlid  11532  recex  11988  btwnz  12842  lbzbi  13103  qbtwnre  13369  caubnd  15570  divalglem9  16615  unbenlem  17130  firest  17653  imasmnd2  19018  imasgrp2  19315  pmtrfrn  19723  pgpfi  19870  sylow2blem3  19887  imasrng  20450  imasring  20611  lspsneq  21451  lspdisj  21454  elcls  23446  elcls3  23456  subbascn  23627  cmpsublem  23772  cmpsub  23773  nllyidm  23863  comppfsc  23906  ptpjopn  23986  fbfinnfr  24215  filin  24228  isfil2  24230  infil  24237  fgss2  24248  fgfil  24249  fgcl  24252  fgabs  24253  elfm2  24322  rnelfm  24327  fmfnfmlem2  24329  fmfnfmlem4  24331  fmco  24335  flffbas  24369  cnpflf2  24374  fclscf  24399  alexsubALTlem2  24422  alexsubALTlem3  24423  alexsubALTlem4  24424  alexsubALT  24425  neibl  24875  met2ndc  24897  metcnp3  24914  icccmplem2  25198  xrge0tsms  25209  fgcfil  25647  volfiniun  25923  dyadmax  25974  dyadmbllem  25975  c1liplem1  26371  dgrlem  26603  axcontlem10  29608  usgredg2vtxeuALT  29860  ushgredgedg  29867  ushgredgedgloop  29869  uhgrspan1  29941  nbuhgr2vtx1edgblem  29989  erclwwlksym  30669  erclwwlknsym  30718  umgr2cycllem  30803  umgr2cycl  30804  1pthon2v  30811  conngrv2edg  30853  lpni  31139  grpoidinvlem3  31165  grporcan  31177  omlsii  32062  spansncol  32227  spansnss  32230  spanunsni  32238  h1datomi  32240  nmopsetretALT  32522  branmfn  32764  chjatom  33016  cvbr4i  33026  atomli  33041  xrge0tsmsd  33733  sat1el2xp  36352  fmlasuc  36359  satffunlem1lem2  36376  satffunlem2lem1  36377  satffunlem2lem2  36379  dfon2lem6  36765  colineardim1  37041  finminlem  37321  nn0prpwlem  37325  neibastop2lem  37363  neibastop2  37364  fgmin  37373  exrecfnlem  38570  heiborlem10  39020  prtlem15  40198  lshpcmp  40311  lsatn0  40322  lsatcmp  40326  lsmsat  40331  lsatcv0  40354  l1cvpat  40377  eqlkr  40422  lshpkrlem1  40433  lshpkrlem6  40438  lfl1dim  40444  lfl1dim2N  40445  lkrss2N  40492  athgt  40779  3dim2  40791  llnle  40841  llncmp  40845  lplnle  40863  lplnnle2at  40864  llncvrlpln2  40880  llncvrlpln  40881  lplncmp  40885  lplnexllnN  40887  lvolnle3at  40905  lplncvrlvol2  40938  lplncvrlvol  40939  lvolcmp  40940  pointpsubN  41074  pclfinN  41223  pclfinclN  41273  osumcllem11N  41289  pexmidlem4N  41296  cdleme17d3  41819  cdlemeg46gfre  41855  cdleme48gfv1  41859  cdleme50trn2  41874  trlord  41892  cdlemg6e  41945  cdlemj3  42146  diaelrnN  42368  diaintclN  42381  dia2dimlem6  42392  cdlemm10N  42441  dibintclN  42490  dihord6apre  42579  dihord5b  42582  dihord5apre  42585  dihglblem5apreN  42614  dihglblem2N  42617  dihglblem3N  42618  dihglbcpreN  42623  dihintcl  42667  lclkrlem2y  42854  lcfrvalsnN  42864  isnacs3  43987  jm2.26  44275  hbtlem5  44395  dflim5  44592  uzwo4  46344  iunincfi  46382  restuni3  46406  disjinfi  46480  ssnnf1octb  46482  choicefi  46487  mapssbi  46499  unirnmapsn  46500  iunmapsn  46503  supxrgere  46618  supxrgelem  46622  suplesup  46624  infleinf  46656  suplesup2  46660  rexabslelem  46701  islptre  46904  limcperiod  46913  limclner  46934  limsupmnfuzlem  47009  limsupre3lem  47015  coskpi2  47149  cosknegpi  47152  icccncfext  47170  stoweidlem27  47310  stoweidlem59  47342  fourierdlem41  47431  fourierdlem42  47432  fourierdlem70  47459  fourierdlem71  47460  fourierdlem81  47470  fourierswlem  47513  qndenserrnopnlem  47580  subsaliuncl  47641  subsalsal  47642  sge0tsms  47663  sge0fsum  47670  sge0supre  47672  sge0sup  47674  sge0rnbnd  47676  sge0pnffigt  47679  sge0resrn  47687  sge0split  47692  sge0iunmptlemfi  47696  sge0rpcpnf  47704  sge0isum  47710  sge0xaddlem2  47717  sge0uzfsumgt  47727  sge0seq  47729  sge0reuz  47730  nnfoctbdjlem  47738  nnfoctbdj  47739  meadjiunlem  47748  meaiuninclem  47763  carageniuncllem2  47805  caratheodorylem2  47810  ovnsupge0  47840  ovncvrrp  47847  hoidmv1lelem3  47876  hoidmv1le  47877  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem3  47880  ovnhoilem2  47885  opnvonmbllem2  47916  ovnovollem3  47941  smfpimbor1lem1  48081  smfco  48085  smfpimcc  48091  smfinflem  48100  nprmmul3  48884  fmtno4prmfac  48930  sfprmdvdsmersenne  48961  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  bgoldbtbnd  49180  grimuhgr  49258  clnbgrgrim  49305  uspgrlimlem2  49360