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

Theorem rexlimiv 3239
 Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)
Hypothesis
Ref Expression
rexlimiv.1 (𝑥𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rexlimiv (∃𝑥𝐴 𝜑𝜓)
Distinct variable group:   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimiv
StepHypRef Expression
1 rexlimiv.1 . . 3 (𝑥𝐴 → (𝜑𝜓))
21rgen 3116 . 2 𝑥𝐴 (𝜑𝜓)
3 r19.23v 3238 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑𝜓))
42, 3mpbi 233 1 (∃𝑥𝐴 𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107 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 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112 This theorem is referenced by:  rexlimiva  3240  rexlimivw  3241  rexlimdv  3242  rexlimivv  3251  rexn0  4412  issn  4723  uniss2  4834  disjiun  5018  reuop  6113  ssimaex  6724  ordzsl  7543  onzsl  7544  mpoexw  7762  fsplitfpar  7800  tfrlem8  8006  nneob  8265  ecoptocl  8373  elixpsn  8487  ixpsnf1o  8488  php  8688  php3  8690  ssfi  8725  findcard  8744  findcard2  8745  ordunifi  8755  fiint  8782  en3lp  9064  inf0  9071  inf3lemd  9077  inf3lem6  9083  noinfep  9110  cantnfvalf  9115  trcl  9157  bndrank  9257  rankc2  9287  tcrank  9300  ficardom  9377  ac10ct  9448  isinfcard  9506  alephfp  9522  dfac5lem4  9540  dfac2b  9544  ackbij2  9657  fin23lem16  9749  fin23lem29  9755  fin17  9808  fin1a2lem6  9819  itunitc  9835  hsmexlem9  9839  axdc3lem2  9865  axdc3lem4  9867  axcclem  9871  zorn2lem7  9916  wunr1om  10133  tskr1om  10181  grothomex  10243  prnmadd  10411  ltaprlem  10458  mulgt0sr  10519  0cnALT2  10867  renegcli  10939  peano2nn  11640  bndndx  11887  uzn0  12251  ublbneg  12324  om2uzrani  13318  uzrdgfni  13324  exprelprel  13846  rtrclreclem3  14414  rtrclind  14419  rexanuz2  14704  caurcvg  15028  caucvg  15030  infcvgaux1i  15207  vdwlem6  16315  dfgrp2e  18125  efgrelexlemb  18872  cygth  20268  psgnghm  20274  iscldtop  21710  opnneiid  21741  pnfnei  21835  mnfnei  21836  discmp  22013  cmpsublem  22014  cmpfi  22023  2ndcredom  22065  2ndc1stc  22066  2ndcdisj  22071  kgenidm  22162  methaus  23137  xrtgioo  23421  caun0  23895  ovolmge0  24091  itg2lcl  24341  aannenlem2  24935  aannenlem3  24936  aaliou2  24946  2lgslem1b  25986  2sqlem2  26012  ostth  26233  midwwlks2s3  27748  3cyclfrgrrn1  28080  3cyclfrgrrn  28081  h1de2ctlem  29348  h1de2ci  29349  spansni  29350  spanunsni  29372  riesz3i  29855  adjbd1o  29878  rnbra  29900  pjnmopi  29941  dfpjop  29975  atom1d  30146  cvexchlem  30161  cdj1i  30226  cdj3lem1  30227  hasheuni  31469  cvmlift2lem12  32689  satfrnmapom  32745  sat1el2xp  32754  fmla1  32762  gonar  32770  goalr  32772  fmla0disjsuc  32773  mrsubccat  32893  msrid  32920  elmthm  32951  untint  33066  dfon2lem3  33158  dfon2lem7  33162  dfrdg2  33168  trpred0  33203  nodmon  33285  sltval2  33291  bdayfo  33310  finminlem  33794  fneint  33824  ptrecube  35076  poimirlem26  35102  poimirlem27  35103  poimirlem29  35105  poimirlem30  35106  zerdivemp1x  35404  dochsnnz  38765  ismrc  39685  eldiophb  39741  eldioph4b  39795  dfacbasgrp  40095  dfsucon  40274  subsaliuncllem  43040  icoresmbl  43225  elsetpreimafvssdm  43946  sprsymrelfvlem  44050  sprsymrelf1lem  44051  prmdvdsfmtnof1lem2  44145  uspgropssxp  44415  0aryfvalel  45089
 Copyright terms: Public domain W3C validator