Theorem rexlimdv 3214

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-ral 3071  df-rex 3072

This theorem is referenced by:  rexlimdva  3215  rexlimdv3a  3217  rexlimdva2  3218  rexlimdvw  3221  rexlimdvv  3224  elpwunsn  4625  eldmrexrnb  6963  weniso  7219  ssorduni  7621  onint  7632  limuni3  7691  peano5  7732  funcnvuni  7770  funeldmdif  7880  frxp  7956  smoiun  8181  tfrlem9  8205  oaordex  8372  oalimcl  8374  oaass  8375  findcard2  8927  findcard3  9033  frfi  9035  unblem1  9042  ordiso2  9250  inf3lem3  9364  trpredrec  9482  r1sdom  9531  tz9.12lem3  9546  karden  9652  infxpenlem  9768  cardinfima  9852  iunfictbso  9869  dfac5  9883  cfcoflem  10027  fin23lem11  10072  fin23lem30  10097  fin1a2lem13  10167  axdc3lem2  10206  konigthlem  10323  fpwwe2lem11  10396  tskuni  10538  axgroth6  10583  nqereu  10684  genpnmax  10762  ltaddpr  10789  recexsrlem  10858  mulgt0sr  10860  axrrecex  10918  axpre-sup  10924  addid1  11153  addid2  11156  recex  11605  btwnz  12420  lbzbi  12673  qbtwnre  12930  caubnd  15066  divalglem9  16106  unbenlem  16605  firest  17139  imasmnd2  18418  imasgrp2  18686  pmtrfrn  19062  pgpfi  19206  sylow2blem3  19223  imasring  19854  lspsneq  20380  lspdisj  20383  elcls  22220  elcls3  22230  subbascn  22401  cmpsublem  22546  cmpsub  22547  nllyidm  22636  comppfsc  22679  ptpjopn  22759  fbfinnfr  22988  filin  23001  isfil2  23003  infil  23010  fgss2  23021  fgfil  23022  fgcl  23025  fgabs  23026  elfm2  23095  rnelfm  23100  fmfnfmlem2  23102  fmfnfmlem4  23104  fmco  23108  flffbas  23142  cnpflf2  23147  fclscf  23172  alexsubALTlem2  23195  alexsubALTlem3  23196  alexsubALTlem4  23197  alexsubALT  23198  neibl  23653  met2ndc  23675  metcnp3  23692  icccmplem2  23982  xrge0tsms  23993  fgcfil  24431  volfiniun  24707  dyadmax  24758  dyadmbllem  24759  c1liplem1  25156  dgrlem  25386  axcontlem10  27337  usgredg2vtxeuALT  27585  ushgredgedg  27592  ushgredgedgloop  27594  uhgrspan1  27666  nbuhgr2vtx1edgblem  27714  erclwwlksym  28379  erclwwlknsym  28428  1pthon2v  28511  conngrv2edg  28553  lpni  28836  grpoidinvlem3  28862  grporcan  28874  omlsii  29759  spansncol  29924  spansnss  29927  spanunsni  29935  h1datomi  29937  nmopsetretALT  30219  branmfn  30461  chjatom  30713  cvbr4i  30723  atomli  30738  xrge0tsmsd  31311  umgr2cycllem  33096  umgr2cycl  33097  sat1el2xp  33335  fmlasuc  33342  satffunlem1lem2  33359  satffunlem2lem1  33360  satffunlem2lem2  33362  onelssex  33655  dfon2lem6  33758  colineardim1  34357  finminlem  34501  nn0prpwlem  34505  neibastop2lem  34543  neibastop2  34544  fgmin  34553  exrecfnlem  35544  heiborlem10  35972  prtlem15  36883  lshpcmp  36996  lsatn0  37007  lsatcmp  37011  lsmsat  37016  lsatcv0  37039  l1cvpat  37062  eqlkr  37107  lshpkrlem1  37118  lshpkrlem6  37123  lfl1dim  37129  lfl1dim2N  37130  lkrss2N  37177  athgt  37464  3dim2  37476  llnle  37526  llncmp  37530  lplnle  37548  lplnnle2at  37549  llncvrlpln2  37565  llncvrlpln  37566  lplncmp  37570  lplnexllnN  37572  lvolnle3at  37590  lplncvrlvol2  37623  lplncvrlvol  37624  lvolcmp  37625  pointpsubN  37759  pclfinN  37908  pclfinclN  37958  osumcllem11N  37974  pexmidlem4N  37981  cdleme17d3  38504  cdlemeg46gfre  38540  cdleme48gfv1  38544  cdleme50trn2  38559  trlord  38577  cdlemg6e  38630  cdlemj3  38831  diaelrnN  39053  diaintclN  39066  dia2dimlem6  39077  cdlemm10N  39126  dibintclN  39175  dihord6apre  39264  dihord5b  39267  dihord5apre  39270  dihglblem5apreN  39299  dihglblem2N  39302  dihglblem3N  39303  dihglbcpreN  39308  dihintcl  39352  lclkrlem2y  39539  lcfrvalsnN  39549  isnacs3  40527  jm2.26  40819  fnwe2lem2  40871  hbtlem5  40948  uzwo4  42569  iunincfi  42612  restuni3  42635  disjinfi  42699  ssnnf1octb  42701  choicefi  42708  mapssbi  42721  unirnmapsn  42722  ssmapsn  42724  iunmapsn  42725  supxrgere  42841  supxrgelem  42845  suplesup  42847  infleinf  42880  suplesup2  42884  rexabslelem  42927  islptre  43129  limcperiod  43138  limclner  43161  limsupmnfuzlem  43236  limsupre3lem  43242  coskpi2  43376  cosknegpi  43379  icccncfext  43397  stoweidlem27  43537  stoweidlem59  43569  fourierdlem41  43658  fourierdlem42  43659  fourierdlem70  43686  fourierdlem71  43687  fourierdlem81  43697  fourierswlem  43740  qndenserrnopnlem  43807  subsaliuncl  43866  subsalsal  43867  sge0tsms  43887  sge0fsum  43894  sge0supre  43896  sge0sup  43898  sge0rnbnd  43900  sge0pnffigt  43903  sge0resrn  43911  sge0split  43916  sge0iunmptlemfi  43920  sge0rpcpnf  43928  sge0isum  43934  sge0xaddlem2  43941  sge0uzfsumgt  43951  sge0seq  43953  sge0reuz  43954  nnfoctbdjlem  43962  nnfoctbdj  43963  meadjiunlem  43972  meaiuninclem  43987  carageniuncllem2  44029  caratheodorylem2  44034  ovnsupge0  44064  ovncvrrp  44071  hoidmv1lelem3  44100  hoidmv1le  44101  hoidmvlelem1  44102  hoidmvlelem2  44103  hoidmvlelem3  44104  ovnhoilem2  44109  opnvonmbllem2  44140  ovolval5lem3  44161  ovnovollem3  44165  sssmf  44240  smfpimbor1lem1  44298  smfco  44302  smfpimcc  44307  smfinflem  44316  fmtno4prmfac  44991  sfprmdvdsmersenne  45022  nnsum4primeseven  45219  nnsum4primesevenALTV  45220  bgoldbtbnd  45228