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  2108  ax11el  2109  axext4  2240  eqrdv  2254  abbi2dv  2371  abbi1dv  2372  elex22  2751  elex2  2752  cla4imdv  2816  pm13.183  2859  moeq3  2893  sbc2or  2943  sbcthdv  2950  sbcimdv  2996  ssrdv  3127  ss2abdv  3188  abssdv  3189  dfnfc2  3786  intss  3824  intab  3833  dfiin2g  3877  disjss1  3939  mpteq12dva  4037  axsep  4080  el  4130  euotd  4204  reusv1  4471  reusv2lem1  4472  reusv2lem2  4473  tfisi  4586  limom  4608  ssrelrel  4740  issref  5009  asymref2  5013  funmo  5175  funco  5195  funun  5199  fununi  5219  funcnvuni  5220  nfunsn  5457  funoprabg  5842  1stconst  6106  2ndconst  6107  frxp  6124  fnwelem  6129  iotaval  6201  iota5  6210  iotabidv  6211  seqomlem2  6396  iserd  6619  findcard3  7033  frfi  7035  fiint  7066  dffi2  7109  hartogslem1  7190  wdomd  7228  ixpiunwdom  7238  sucprcreg  7246  rankval3b  7431  fseqenlem2  7585  dfac3  7681  dfac5  7688  dfac2  7690  dfac8  7694  dfac9  7695  dfacacn  7700  dfac13  7701  kmlem1  7709  kmlem6  7714  kmlem13  7721  fin23lem32  7903  axdc2lem  8007  zornn0g  8065  brdom6disj  8090  fpwwe2lem11  8195  fpwwe2lem12  8196  fpwwe2lem13  8197  hargch  8232  alephgch  8233  nqpr  8571  reclem2pr  8605  shftfn  11498  fsumiunOLD  12211  hashiunOLD  12212  ramub  12987  ramcl  13003  imasaddfnlem  13357  imasvscafn  13366  mrieqv2d  13468  mreexexd  13477  catideu  13504  invfun  13593  mreclat  14217  letsr  14276  efgval  14953  efgi  14955  efgi2  14961  gsumval3  15118  gsumzaddlem  15130  pgpfac1lem5  15241  islbs3  15835  lbsextlem4  15841  mplsubglem  16106  mpllsslem  16107  cssmre  16520  obslbs  16557  tgcl  16634  indistopon  16665  ppttop  16671  epttop  16673  mretopd  16756  toponmre  16757  neissex  16791  lmfun  17036  2ndcdisj  17109  1stccnp  17115  kgentopon  17160  dfac14  17239  ptcnp  17243  uptx  17246  ptrescn  17260  qtoptop2  17317  filcon  17505  filssufilg  17533  rnelfmlem  17574  alexsubALTlem2  17669  prdsxmslem2  18002  mbfposr  18934  mbfinf  18947  i1fd  18963  itg1climres  18996  perfdvf  19180  evlseu  19327  taylf  19667  ex-natded9.26  20759  ex-natded9.26-2  20760  nmcexi  22531  relexpindlem  23373  rtrclreclem.min  23381  dfrtrcl2  23382  dfpo2  23448  dfon2lem6  23478  dfon2lem8  23480  dfon2lem9  23481  dfon2  23482  elfuns  23794  mptelee  23863  eqintg  24292  inposet  24610  inttop2  24847  intopcoaconb  24872  qusp  24874  prcnt  24883  ismonc  25146  isepic  25156  bosser  25499  trer  25559  finminlem  25563  neibastop1  25640  neibastop3  25643  upixp  25735  prter1  26079  ismrcd1  26105  ttac  26461  fnwe2  26482  aomclem6  26488  dfac11  26492  dfac21  26496  frlmup4  26585  hbtlem2  26660  sbeqalbi  26932  ax10ext  26938  ax10-16  26939  pm13.192  26943  pm14.24  26965  sbcss  27322  gen11  27401  trsspwALT2  27606  snssiALT  27616  sstrALT2  27624  en3lpVD  27634  sspwimp  27707  sspwimpcf  27709  sspwimpALT  27714  sspwimpALT2  27718  a9e2ndeqALT  27721  bnj145  27767  bnj1143  27834  bnj1379  27875  bnj149  27919
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