MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimdv Structured version   Visualization version   GIF version

Theorem rexlimdv 3275
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
StepHypRef Expression
1 rexlimdv.1 . . . 4 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
21com3l 89 . . 3 (𝑥𝐴 → (𝜓 → (𝜑𝜒)))
32rexlimiv 3272 . 2 (∃𝑥𝐴 𝜓 → (𝜑𝜒))
43com12 32 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  wrex 3134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3138  df-rex 3139
This theorem is referenced by:  rexlimdva  3276  rexlimdv3a  3278  rexlimdva2  3279  rexlimdvw  3282  rexlimdvv  3285  elpwunsn  4606  eldmrexrnb  6849  weniso  7100  ssorduni  7494  onint  7504  limuni3  7561  funcnvuni  7631  funeldmdif  7742  frxp  7816  smoiun  7994  tfrlem9  8017  oaordex  8180  oalimcl  8182  oaass  8183  findcard3  8758  frfi  8760  unblem1  8767  ordiso2  8976  inf3lem3  9090  r1sdom  9200  tz9.12lem3  9215  karden  9321  infxpenlem  9437  cardinfima  9521  iunfictbso  9538  dfac5  9552  cfcoflem  9692  fin23lem11  9737  fin23lem30  9762  fin1a2lem13  9832  axdc3lem2  9871  konigthlem  9988  fpwwe2lem12  10061  tskuni  10203  axgroth6  10248  nqereu  10349  genpnmax  10427  ltaddpr  10454  recexsrlem  10523  mulgt0sr  10525  axrrecex  10583  axpre-sup  10589  addid1  10818  addid2  10821  recex  11270  btwnz  12081  lbzbi  12333  qbtwnre  12589  caubnd  14718  divalglem9  15750  unbenlem  16242  firest  16706  imasmnd2  17948  imasgrp2  18214  pmtrfrn  18586  pgpfi  18730  sylow2blem3  18747  imasring  19372  lspsneq  19894  lspdisj  19897  elcls  21685  elcls3  21695  subbascn  21866  cmpsublem  22011  cmpsub  22012  nllyidm  22101  comppfsc  22144  ptpjopn  22224  fbfinnfr  22453  filin  22466  isfil2  22468  infil  22475  fgss2  22486  fgfil  22487  fgcl  22490  fgabs  22491  elfm2  22560  rnelfm  22565  fmfnfmlem2  22567  fmfnfmlem4  22569  fmco  22573  flffbas  22607  cnpflf2  22612  fclscf  22637  alexsubALTlem2  22660  alexsubALTlem3  22661  alexsubALTlem4  22662  alexsubALT  22663  neibl  23115  met2ndc  23137  metcnp3  23154  icccmplem2  23435  xrge0tsms  23446  fgcfil  23882  volfiniun  24158  dyadmax  24209  dyadmbllem  24210  c1liplem1  24606  dgrlem  24833  axcontlem10  26774  usgredg2vtxeuALT  27019  ushgredgedg  27026  ushgredgedgloop  27028  uhgrspan1  27100  nbuhgr2vtx1edgblem  27148  erclwwlksym  27813  erclwwlknsym  27862  1pthon2v  27945  conngrv2edg  27987  lpni  28270  grpoidinvlem3  28296  grporcan  28308  omlsii  29193  spansncol  29358  spansnss  29361  spanunsni  29369  h1datomi  29371  nmopsetretALT  29653  branmfn  29895  chjatom  30147  cvbr4i  30157  atomli  30172  xrge0tsmsd  30728  umgr2cycllem  32448  umgr2cycl  32449  sat1el2xp  32687  fmlasuc  32694  satffunlem1lem2  32711  satffunlem2lem1  32712  satffunlem2lem2  32714  dfon2lem6  33094  trpredrec  33138  colineardim1  33583  finminlem  33727  nn0prpwlem  33731  neibastop2lem  33769  neibastop2  33770  fgmin  33779  exrecfnlem  34745  heiborlem10  35207  prtlem15  36120  lshpcmp  36233  lsatn0  36244  lsatcmp  36248  lsmsat  36253  lsatcv0  36276  l1cvpat  36299  eqlkr  36344  lshpkrlem1  36355  lshpkrlem6  36360  lfl1dim  36366  lfl1dim2N  36367  lkrss2N  36414  athgt  36701  3dim2  36713  llnle  36763  llncmp  36767  lplnle  36785  lplnnle2at  36786  llncvrlpln2  36802  llncvrlpln  36803  lplncmp  36807  lplnexllnN  36809  lvolnle3at  36827  lplncvrlvol2  36860  lplncvrlvol  36861  lvolcmp  36862  pointpsubN  36996  pclfinN  37145  pclfinclN  37195  osumcllem11N  37211  pexmidlem4N  37218  cdleme17d3  37741  cdlemeg46gfre  37777  cdleme48gfv1  37781  cdleme50trn2  37796  trlord  37814  cdlemg6e  37867  cdlemj3  38068  diaelrnN  38290  diaintclN  38303  dia2dimlem6  38314  cdlemm10N  38363  dibintclN  38412  dihord6apre  38501  dihord5b  38504  dihord5apre  38507  dihglblem5apreN  38536  dihglblem2N  38539  dihglblem3N  38540  dihglbcpreN  38545  dihintcl  38589  lclkrlem2y  38776  lcfrvalsnN  38786  isnacs3  39572  jm2.26  39864  fnwe2lem2  39916  hbtlem5  39993  uzwo4  41612  iunincfi  41657  restuni3  41680  disjinfi  41750  ssnnf1octb  41752  choicefi  41759  mapssbi  41772  unirnmapsn  41773  ssmapsn  41775  iunmapsn  41776  supxrgere  41896  supxrgelem  41900  suplesup  41902  infleinf  41935  suplesup2  41939  rexabslelem  41986  islptre  42192  limcperiod  42201  limclner  42224  limsupmnfuzlem  42299  limsupre3lem  42305  coskpi2  42439  cosknegpi  42442  icccncfext  42460  stoweidlem27  42600  stoweidlem59  42632  fourierdlem41  42721  fourierdlem42  42722  fourierdlem70  42749  fourierdlem71  42750  fourierdlem81  42760  fourierswlem  42803  qndenserrnopnlem  42870  subsaliuncl  42929  subsalsal  42930  sge0tsms  42950  sge0fsum  42957  sge0supre  42959  sge0sup  42961  sge0rnbnd  42963  sge0pnffigt  42966  sge0resrn  42974  sge0split  42979  sge0iunmptlemfi  42983  sge0rpcpnf  42991  sge0isum  42997  sge0xaddlem2  43004  sge0uzfsumgt  43014  sge0seq  43016  sge0reuz  43017  nnfoctbdjlem  43025  nnfoctbdj  43026  meadjiunlem  43035  meaiuninclem  43050  carageniuncllem2  43092  caratheodorylem2  43097  ovnsupge0  43127  ovncvrrp  43134  hoidmv1lelem3  43163  hoidmv1le  43164  hoidmvlelem1  43165  hoidmvlelem2  43166  hoidmvlelem3  43167  ovnhoilem2  43172  opnvonmbllem2  43203  ovolval5lem3  43224  ovnovollem3  43228  sssmf  43303  smfpimbor1lem1  43361  smfco  43365  smfpimcc  43370  smfinflem  43379  fmtno4prmfac  44020  sfprmdvdsmersenne  44052  nnsum4primeseven  44249  nnsum4primesevenALTV  44250  bgoldbtbnd  44258
  Copyright terms: Public domain W3C validator