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

Theorem rexlimdv 3012
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 87 . . 3 (𝑥𝐴 → (𝜓 → (𝜑𝜒)))
32rexlimiv 3009 . 2 (∃𝑥𝐴 𝜓 → (𝜑𝜒))
43com12 32 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  wrex 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902
This theorem is referenced by:  rexlimdva  3013  rexlimdv3a  3015  rexlimdvw  3016  rexlimdvv  3019  elpwunsn  4171  trintss  4697  eldmrexrnb  6274  dffo3  6282  weniso  6504  ssorduni  6877  onint  6887  limuni3  6944  funcnvuni  7012  frxp  7174  smoiun  7345  tfrlem9  7368  oaordex  7525  oalimcl  7527  oaass  7528  omlimcl  7545  findcard3  8088  frfi  8090  unblem1  8097  ordiso2  8303  inf3lem3  8410  r1sdom  8520  tz9.12lem3  8535  karden  8641  infxpenlem  8719  cardinfima  8803  iunfictbso  8820  dfac5  8834  cfflb  8964  cfcoflem  8977  cfcof  8979  fin23lem11  9022  fin23lem30  9047  fin1a2lem13  9117  axdc3lem2  9156  konigthlem  9269  alephval2  9273  pwcfsdom  9284  fpwwe2lem12  9342  tskuni  9484  axgroth6  9529  nqereu  9630  genpnmax  9708  ltaddpr  9735  recexsrlem  9803  mulgt0sr  9805  recexsr  9807  axrrecex  9863  axpre-sup  9869  addid1  10095  addid2  10098  recex  10538  zdiv  11323  btwnz  11355  lbzbi  11652  qbtwnre  11904  caubnd  13946  divalglem9  14962  unbenlem  15450  firest  15916  imasmnd2  17150  imasgrp2  17353  pmtrfrn  17701  pgpfi  17843  sylow2blem3  17860  imasring  18442  lspsneq  18943  lspdisj  18946  fctop  20618  cctop  20620  elcls  20687  elcls3  20697  subbascn  20868  cmpsublem  21012  cmpsub  21013  nllyidm  21102  comppfsc  21145  ptpjopn  21225  fbfinnfr  21455  filin  21468  isfil2  21470  infil  21477  fgss2  21488  fgfil  21489  fgcl  21492  fgabs  21493  elfm2  21562  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  fmco  21575  flffbas  21609  cnpflf2  21614  fclscf  21639  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  neibl  22116  met2ndc  22138  metcnp3  22155  icccmplem2  22434  xrge0tsms  22445  fgcfil  22877  volfiniun  23122  dyadmax  23172  dyadmbllem  23173  c1liplem1  23563  dgrlem  23789  axcontlem10  25653  usgrarnedg  25913  erclwwlksym  26342  erclwwlknsym  26354  lpni  26722  grpoidinvlem3  26744  grporcan  26756  grpoinvf  26770  nmosetre  27003  omlsii  27646  spansncol  27811  spansnss  27814  normcan  27819  spanunsni  27822  h1datomi  27824  nmopsetretALT  28106  nmfnsetre  28120  branmfn  28348  superpos  28597  chjatom  28600  cvbr4i  28610  atomli  28625  xrge0tsmsd  29116  eulerpartlemgh  29767  dfon2lem6  30937  trpredrec  30982  colineardim1  31338  finminlem  31482  nn0prpwlem  31487  neibastop2lem  31525  neibastop2  31526  fgmin  31535  heiborlem10  32789  prtlem15  33178  lshpcmp  33293  lsatn0  33304  lsatcmp  33308  lsmsat  33313  lsatcv0  33336  l1cvpat  33359  eqlkr  33404  lshpkrlem1  33415  lshpkrlem6  33420  lfl1dim  33426  lfl1dim2N  33427  lkrss2N  33474  athgt  33760  3dim2  33772  llnle  33822  llncmp  33826  lplnle  33844  lplnnle2at  33845  llncvrlpln2  33861  llncvrlpln  33862  lplncmp  33866  lplnexllnN  33868  lvolnle3at  33886  lplncvrlvol2  33919  lplncvrlvol  33920  lvolcmp  33921  pointpsubN  34055  pclfinN  34204  pclfinclN  34254  osumcllem11N  34270  pexmidlem4N  34277  cdleme17d3  34802  cdlemeg46gfre  34838  cdleme48gfv1  34842  cdleme50trn2  34857  trlord  34875  cdlemg6e  34928  cdlemj3  35129  diaelrnN  35352  diaintclN  35365  dia2dimlem6  35376  cdlemm10N  35425  dibintclN  35474  dihord6apre  35563  dihord5b  35566  dihord5apre  35569  dihglblem5apreN  35598  dihglblem2N  35601  dihglblem3N  35602  dihglbcpreN  35607  dihintcl  35651  lclkrlem2y  35838  lcfrvalsnN  35848  isnacs3  36291  jm2.26  36587  fnwe2lem2  36639  hbtlem5  36717  uzwo4  38246  iunincfi  38300  eliuniin  38307  restuni3  38333  disjinfi  38375  ssnnf1octb  38377  mapsnd  38383  choicefi  38387  mapssbi  38400  unirnmapsn  38401  ssmapsn  38403  iunmapsn  38404  supxrgere  38490  supxrgelem  38494  suplesup  38496  infleinf  38529  suplesup2  38533  islptre  38686  limcperiod  38695  limclner  38718  coskpi2  38749  cosknegpi  38752  icccncfext  38773  stoweidlem27  38920  stoweidlem59  38952  fourierdlem41  39041  fourierdlem42  39042  fourierdlem70  39069  fourierdlem71  39070  fourierdlem81  39080  fourierswlem  39123  qndenserrnopnlem  39193  subsaliuncl  39252  subsalsal  39253  sge0tsms  39273  sge0fsum  39280  sge0supre  39282  sge0sup  39284  sge0rnbnd  39286  sge0pnffigt  39289  sge0resrn  39297  sge0split  39302  sge0iunmptlemfi  39306  sge0rpcpnf  39314  sge0isum  39320  sge0xaddlem2  39327  sge0uzfsumgt  39337  sge0seq  39339  sge0reuz  39340  nnfoctbdjlem  39348  nnfoctbdj  39349  meadjiunlem  39358  meaiuninclem  39373  carageniuncllem2  39412  caratheodorylem2  39417  ovnsupge0  39447  ovncvrrp  39454  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnhoilem2  39492  opnvonmbllem2  39523  ovolval5lem3  39544  ovnovollem3  39548  sssmf  39625  smflimlem4  39660  smfpimbor1lem1  39683  smfco  39687  fmtno4prmfac  40022  sfprmdvdsmersenne  40058  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbnd  40225  usgredg2vtxeuALT  40449  ushgredgedga  40456  ushgredgedgaloop  40458  uhgrspan1  40527  nbuhgr2vtx1edgblem  40573  erclwwlkssym  41242  erclwwlksnsym  41254  1pthon2v-av  41320  conngrv2edg  41362  islindeps2  42066
  Copyright terms: Public domain W3C validator