MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  alrimiv Unicode version

Theorem alrimiv 2013
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
alrimiv.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
alrimiv  |-  ( ph  ->  A. x ps )
Distinct variable group:    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem alrimiv
StepHypRef Expression
1 nfv 1629 . 2  |-  F/ x ph
2 alrimiv.1 . 2  |-  ( ph  ->  ps )
31, 2alrimi 1706 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532
This theorem is referenced by:  alrimivv  2014  nfdv  2016  cbvald  2052  ax11eq  2109  ax11el  2110  axext4  2242  eqrdv  2256  abbi2dv  2373  abbi1dv  2374  elex22  2774  elex2  2775  cla4imdv  2840  pm13.183  2883  moeq3  2917  sbc2or  2974  sbcthdv  2981  sbcimdv  3027  ssrdv  3160  ss2abdv  3221  abssdv  3222  dfnfc2  3819  intss  3857  intab  3866  dfiin2g  3910  disjss1  3973  mpteq12dva  4071  axsep  4114  el  4164  euotd  4239  reusv1  4506  reusv2lem1  4507  reusv2lem2  4508  tfisi  4621  limom  4643  ssrelrel  4775  issref  5044  asymref2  5048  funmo  5210  funco  5230  funun  5234  fununi  5254  funcnvuni  5255  nfunsn  5492  funoprabg  5877  1stconst  6141  2ndconst  6142  frxp  6159  fnwelem  6164  iotaval  6236  iota5  6245  iotabidv  6246  seqomlem2  6431  iserd  6654  findcard3  7068  frfi  7070  fiint  7101  dffi2  7144  hartogslem1  7225  wdomd  7263  ixpiunwdom  7273  sucprcreg  7281  rankval3b  7466  fseqenlem2  7620  dfac3  7716  dfac5  7723  dfac2  7725  dfac8  7729  dfac9  7730  dfacacn  7735  dfac13  7736  kmlem1  7744  kmlem6  7749  kmlem13  7756  fin23lem32  7938  axdc2lem  8042  zornn0g  8100  brdom6disj  8125  fpwwe2lem11  8230  fpwwe2lem12  8231  fpwwe2lem13  8232  hargch  8267  alephgch  8268  nqpr  8606  reclem2pr  8640  shftfn  11534  fsumiunOLD  12247  hashiunOLD  12248  ramub  13023  ramcl  13039  imasaddfnlem  13393  imasvscafn  13402  mrieqv2d  13504  mreexexd  13513  invfun  13629  mreclat  14253  letsr  14312  efgval  14989  efgi  14991  efgi2  14997  gsumval3  15154  gsumzaddlem  15166  pgpfac1lem5  15277  islbs3  15871  lbsextlem4  15877  mplsubglem  16142  mpllsslem  16143  cssmre  16556  obslbs  16593  tgcl  16670  indistopon  16701  ppttop  16707  epttop  16709  mretopd  16792  toponmre  16793  neissex  16827  lmfun  17072  2ndcdisj  17145  1stccnp  17151  kgentopon  17196  dfac14  17275  ptcnp  17279  uptx  17282  ptrescn  17296  qtoptop2  17353  filcon  17541  filssufilg  17569  rnelfmlem  17610  alexsubALTlem2  17705  prdsxmslem2  18038  mbfposr  18970  mbfinf  18983  i1fd  18999  itg1climres  19032  perfdvf  19216  taylf  19703  ex-natded9.26  20795  ex-natded9.26-2  20796  nmcexi  22567  relexpindlem  23409  rtrclreclem.min  23417  dfrtrcl2  23418  dfpo2  23484  dfon2lem6  23514  dfon2lem8  23516  dfon2lem9  23517  dfon2  23518  elfuns  23830  mptelee  23899  eqintg  24328  inposet  24646  inttop2  24883  intopcoaconb  24908  qusp  24910  prcnt  24919  ismonc  25182  isepic  25192  bosser  25535  trer  25595  finminlem  25599  neibastop1  25676  neibastop3  25679  upixp  25771  prter1  26115  ismrcd1  26141  ttac  26497  fnwe2  26518  aomclem6  26524  dfac11  26528  dfac21  26532  hbtlem2  26696  sbeqalbi  26968  ax10ext  26974  ax10-16  26975  pm13.192  26979  pm14.24  27001  itgsinexplem1  27117  sbcss  27442  gen11  27521  trsspwALT2  27726  snssiALT  27736  sstrALT2  27744  en3lpVD  27754  sspwimp  27827  sspwimpcf  27829  sspwimpALT  27834  sspwimpALT2  27838  a9e2ndeqALT  27841  bnj145  27887  bnj1143  27954  bnj1379  27995  bnj149  28039
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-nf 1540
  Copyright terms: Public domain W3C validator