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

Theorem rexlimdv 3011
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 86 . . 3 (𝑥𝐴 → (𝜓 → (𝜑𝜒)))
32rexlimiv 3008 . 2 (∃𝑥𝐴 𝜓 → (𝜑𝜒))
43com12 32 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2900  df-rex 2901
This theorem is referenced by:  rexlimdva  3012  rexlimdv3a  3014  rexlimdvw  3015  rexlimdvv  3018  elpwunsn  4170  trintss  4691  eldmrexrnb  6258  dffo3  6266  weniso  6481  ssorduni  6854  onint  6864  limuni3  6921  funcnvuni  6989  frxp  7151  smoiun  7322  tfrlem9  7345  oaordex  7502  oalimcl  7504  oaass  7505  omlimcl  7522  findcard3  8065  frfi  8067  unblem1  8074  ordiso2  8280  inf3lem3  8387  r1sdom  8497  tz9.12lem3  8512  karden  8618  infxpenlem  8696  cardinfima  8780  iunfictbso  8797  dfac5  8811  cfflb  8941  cfcoflem  8954  cfcof  8956  fin23lem11  8999  fin23lem30  9024  fin1a2lem13  9094  axdc3lem2  9133  konigthlem  9246  alephval2  9250  pwcfsdom  9261  fpwwe2lem12  9319  tskuni  9461  axgroth6  9506  nqereu  9607  genpnmax  9685  ltaddpr  9712  recexsrlem  9780  mulgt0sr  9782  recexsr  9784  axrrecex  9840  axpre-sup  9846  addid1  10067  addid2  10070  recex  10510  zdiv  11281  btwnz  11313  lbzbi  11610  qbtwnre  11865  caubnd  13894  divalglem9  14910  unbenlem  15398  firest  15864  imasmnd2  17098  imasgrp2  17301  pmtrfrn  17649  pgpfi  17791  sylow2blem3  17808  imasring  18390  lspsneq  18891  lspdisj  18894  fctop  20565  cctop  20567  elcls  20634  elcls3  20644  subbascn  20815  cmpsublem  20959  cmpsub  20960  nllyidm  21049  comppfsc  21092  ptpjopn  21172  fbfinnfr  21402  filin  21415  isfil2  21417  infil  21424  fgss2  21435  fgfil  21436  fgcl  21439  fgabs  21440  elfm2  21509  rnelfm  21514  fmfnfmlem2  21516  fmfnfmlem4  21518  fmco  21522  flffbas  21556  cnpflf2  21561  fclscf  21586  alexsubALTlem2  21609  alexsubALTlem3  21610  alexsubALTlem4  21611  alexsubALT  21612  neibl  22063  met2ndc  22085  metcnp3  22102  icccmplem2  22381  xrge0tsms  22392  fgcfil  22821  volfiniun  23066  dyadmax  23116  dyadmbllem  23117  c1liplem1  23507  dgrlem  23733  axcontlem10  25598  usgrarnedg  25706  erclwwlksym  26135  erclwwlknsym  26147  lpni  26515  grpoidinvlem3  26537  grporcan  26549  grpoinvf  26563  nmosetre  26796  omlsii  27439  spansncol  27604  spansnss  27607  normcan  27612  spanunsni  27615  h1datomi  27617  nmopsetretALT  27899  nmfnsetre  27913  branmfn  28141  superpos  28390  chjatom  28393  cvbr4i  28403  atomli  28418  xrge0tsmsd  28909  eulerpartlemgh  29560  dfon2lem6  30730  trpredrec  30775  colineardim1  31131  finminlem  31275  nn0prpwlem  31280  neibastop2lem  31318  neibastop2  31319  fgmin  31328  heiborlem10  32572  prtlem15  32961  lshpcmp  33076  lsatn0  33087  lsatcmp  33091  lsmsat  33096  lsatcv0  33119  l1cvpat  33142  eqlkr  33187  lshpkrlem1  33198  lshpkrlem6  33203  lfl1dim  33209  lfl1dim2N  33210  lkrss2N  33257  athgt  33543  3dim2  33555  llnle  33605  llncmp  33609  lplnle  33627  lplnnle2at  33628  llncvrlpln2  33644  llncvrlpln  33645  lplncmp  33649  lplnexllnN  33651  lvolnle3at  33669  lplncvrlvol2  33702  lplncvrlvol  33703  lvolcmp  33704  pointpsubN  33838  pclfinN  33987  pclfinclN  34037  osumcllem11N  34053  pexmidlem4N  34060  cdleme17d3  34585  cdlemeg46gfre  34621  cdleme48gfv1  34625  cdleme50trn2  34640  trlord  34658  cdlemg6e  34711  cdlemj3  34912  diaelrnN  35135  diaintclN  35148  dia2dimlem6  35159  cdlemm10N  35208  dibintclN  35257  dihord6apre  35346  dihord5b  35349  dihord5apre  35352  dihglblem5apreN  35381  dihglblem2N  35384  dihglblem3N  35385  dihglbcpreN  35390  dihintcl  35434  lclkrlem2y  35621  lcfrvalsnN  35631  isnacs3  36074  jm2.26  36370  fnwe2lem2  36422  hbtlem5  36500  uzwo4  38029  iunincfi  38083  eliuniin  38090  restuni3  38116  disjinfi  38158  ssnnf1octb  38160  mapsnd  38166  choicefi  38170  mapssbi  38183  unirnmapsn  38184  ssmapsn  38186  iunmapsn  38187  supxrgere  38273  supxrgelem  38277  suplesup  38279  infleinf  38312  suplesup2  38316  islptre  38469  limcperiod  38478  limclner  38501  coskpi2  38532  cosknegpi  38535  icccncfext  38556  stoweidlem27  38703  stoweidlem59  38735  fourierdlem41  38824  fourierdlem42  38825  fourierdlem70  38852  fourierdlem71  38853  fourierdlem81  38863  fourierswlem  38906  qndenserrnopnlem  38976  subsaliuncl  39035  subsalsal  39036  sge0tsms  39056  sge0fsum  39063  sge0supre  39065  sge0sup  39067  sge0rnbnd  39069  sge0pnffigt  39072  sge0resrn  39080  sge0split  39085  sge0iunmptlemfi  39089  sge0rpcpnf  39097  sge0isum  39103  sge0xaddlem2  39110  sge0uzfsumgt  39120  sge0seq  39122  sge0reuz  39123  nnfoctbdjlem  39131  nnfoctbdj  39132  meadjiunlem  39141  meaiuninclem  39156  carageniuncllem2  39195  caratheodorylem2  39200  ovnsupge0  39230  ovncvrrp  39237  hoidmv1lelem3  39266  hoidmv1le  39267  hoidmvlelem1  39268  hoidmvlelem2  39269  hoidmvlelem3  39270  ovnhoilem2  39275  opnvonmbllem2  39306  ovolval5lem3  39327  ovnovollem3  39331  sssmf  39408  smflimlem4  39443  smfpimbor1lem1  39466  smfco  39470  fmtno4prmfac  39806  sfprmdvdsmersenne  39842  nnsum4primeseven  40000  nnsum4primesevenALTV  40001  bgoldbtbnd  40009  usgredg2vtxeuALT  40430  ushgredgedga  40437  ushgredgedgaloop  40439  uhgrspan1  40508  nbuhgr2vtx1edgblem  40554  erclwwlkssym  41223  erclwwlksnsym  41235  1pthon2v-av  41301  conngrv2edg  41343  islindeps2  42047
  Copyright terms: Public domain W3C validator