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

Theorem rexlimdv 3059
 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 3056 . 2 (∃𝑥𝐴 𝜓 → (𝜑𝜒))
43com12 32 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2030  ∃wrex 2942 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947 This theorem is referenced by:  rexlimdva  3060  rexlimdv3a  3062  rexlimdvw  3063  rexlimdvv  3066  elpwunsn  4256  trintssOLD  4803  eldmrexrnb  6406  dffo3  6414  weniso  6644  ssorduni  7027  onint  7037  limuni3  7094  funcnvuni  7161  frxp  7332  smoiun  7503  tfrlem9  7526  oaordex  7683  oalimcl  7685  oaass  7686  omlimcl  7703  findcard3  8244  frfi  8246  unblem1  8253  ordiso2  8461  inf3lem3  8565  r1sdom  8675  tz9.12lem3  8690  karden  8796  infxpenlem  8874  cardinfima  8958  iunfictbso  8975  dfac5  8989  cfflb  9119  cfcoflem  9132  cfcof  9134  fin23lem11  9177  fin23lem30  9202  fin1a2lem13  9272  axdc3lem2  9311  konigthlem  9428  alephval2  9432  pwcfsdom  9443  fpwwe2lem12  9501  tskuni  9643  axgroth6  9688  nqereu  9789  genpnmax  9867  ltaddpr  9894  recexsrlem  9962  mulgt0sr  9964  recexsr  9966  axrrecex  10022  axpre-sup  10028  addid1  10254  addid2  10257  recex  10697  zdiv  11485  btwnz  11517  lbzbi  11814  qbtwnre  12068  caubnd  14142  divalglem9  15171  unbenlem  15659  firest  16140  imasmnd2  17374  imasgrp2  17577  pmtrfrn  17924  pgpfi  18066  sylow2blem3  18083  imasring  18665  lspsneq  19170  lspdisj  19173  fctop  20856  cctop  20858  elcls  20925  elcls3  20935  subbascn  21106  cmpsublem  21250  cmpsub  21251  nllyidm  21340  comppfsc  21383  ptpjopn  21463  fbfinnfr  21692  filin  21705  isfil2  21707  infil  21714  fgss2  21725  fgfil  21726  fgcl  21729  fgabs  21730  elfm2  21799  rnelfm  21804  fmfnfmlem2  21806  fmfnfmlem4  21808  fmco  21812  flffbas  21846  cnpflf2  21851  fclscf  21876  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  alexsubALT  21902  neibl  22353  met2ndc  22375  metcnp3  22392  icccmplem2  22673  xrge0tsms  22684  fgcfil  23115  volfiniun  23361  dyadmax  23412  dyadmbllem  23413  c1liplem1  23804  dgrlem  24030  axcontlem10  25898  usgredg2vtxeuALT  26159  ushgredgedg  26166  ushgredgedgloop  26168  uhgrspan1  26240  nbuhgr2vtx1edgblem  26292  erclwwlksym  26978  erclwwlknsym  27034  1pthon2v  27131  conngrv2edg  27173  lpni  27462  grpoidinvlem3  27488  grporcan  27500  grpoinvf  27514  nmosetre  27747  omlsii  28390  spansncol  28555  spansnss  28558  normcan  28563  spanunsni  28566  h1datomi  28568  nmopsetretALT  28850  nmfnsetre  28864  branmfn  29092  superpos  29341  chjatom  29344  cvbr4i  29354  atomli  29369  xrge0tsmsd  29913  eulerpartlemgh  30568  dfon2lem6  31817  trpredrec  31862  colineardim1  32293  finminlem  32437  nn0prpwlem  32442  neibastop2lem  32480  neibastop2  32481  fgmin  32490  heiborlem10  33749  prtlem15  34479  lshpcmp  34593  lsatn0  34604  lsatcmp  34608  lsmsat  34613  lsatcv0  34636  l1cvpat  34659  eqlkr  34704  lshpkrlem1  34715  lshpkrlem6  34720  lfl1dim  34726  lfl1dim2N  34727  lkrss2N  34774  athgt  35060  3dim2  35072  llnle  35122  llncmp  35126  lplnle  35144  lplnnle2at  35145  llncvrlpln2  35161  llncvrlpln  35162  lplncmp  35166  lplnexllnN  35168  lvolnle3at  35186  lplncvrlvol2  35219  lplncvrlvol  35220  lvolcmp  35221  pointpsubN  35355  pclfinN  35504  pclfinclN  35554  osumcllem11N  35570  pexmidlem4N  35577  cdleme17d3  36101  cdlemeg46gfre  36137  cdleme48gfv1  36141  cdleme50trn2  36156  trlord  36174  cdlemg6e  36227  cdlemj3  36428  diaelrnN  36651  diaintclN  36664  dia2dimlem6  36675  cdlemm10N  36724  dibintclN  36773  dihord6apre  36862  dihord5b  36865  dihord5apre  36868  dihglblem5apreN  36897  dihglblem2N  36900  dihglblem3N  36901  dihglbcpreN  36906  dihintcl  36950  lclkrlem2y  37137  lcfrvalsnN  37147  isnacs3  37590  jm2.26  37886  fnwe2lem2  37938  hbtlem5  38015  uzwo4  39535  iunincfi  39586  restuni3  39615  rexlimdva2  39653  disjinfi  39694  ssnnf1octb  39696  mapsnd  39702  choicefi  39706  mapssbi  39719  unirnmapsn  39720  ssmapsn  39722  iunmapsn  39723  supxrgere  39862  supxrgelem  39866  suplesup  39868  infleinf  39901  suplesup2  39905  rexabslelem  39958  islptre  40169  limcperiod  40178  limclner  40201  limsupubuz  40263  limsupmnfuzlem  40276  limsupre3lem  40282  coskpi2  40395  cosknegpi  40398  icccncfext  40418  stoweidlem27  40562  stoweidlem59  40594  fourierdlem41  40683  fourierdlem42  40684  fourierdlem70  40711  fourierdlem71  40712  fourierdlem81  40722  fourierswlem  40765  qndenserrnopnlem  40835  subsaliuncl  40894  subsalsal  40895  sge0tsms  40915  sge0fsum  40922  sge0supre  40924  sge0sup  40926  sge0rnbnd  40928  sge0pnffigt  40931  sge0resrn  40939  sge0split  40944  sge0iunmptlemfi  40948  sge0rpcpnf  40956  sge0isum  40962  sge0xaddlem2  40969  sge0uzfsumgt  40979  sge0seq  40981  sge0reuz  40982  nnfoctbdjlem  40990  nnfoctbdj  40991  meadjiunlem  41000  meaiuninclem  41015  carageniuncllem2  41057  caratheodorylem2  41062  ovnsupge0  41092  ovncvrrp  41099  hoidmv1lelem3  41128  hoidmv1le  41129  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  ovnhoilem2  41137  opnvonmbllem2  41168  ovolval5lem3  41189  ovnovollem3  41193  sssmf  41268  smflimlem4  41303  smfpimbor1lem1  41326  smfco  41330  smfpimcc  41335  smfinflem  41344  fmtno4prmfac  41809  sfprmdvdsmersenne  41845  mogoldbb  41998  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbnd  42022  islindeps2  42597
 Copyright terms: Public domain W3C validator