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

Theorem alrimiv 2012
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  2013  nfdv  2015  cbvald  2051  ax11eq  2105  ax11el  2106  axext4  2237  eqrdv  2251  abbi2dv  2364  abbi1dv  2365  elex22  2738  elex2  2739  cla4imdv  2803  pm13.183  2845  moeq3  2879  sbc2or  2929  sbcthdv  2936  sbcimdv  2982  ssrdv  3106  ss2abdv  3167  abssdv  3168  dfnfc2  3745  intss  3781  intab  3790  dfiin2g  3834  disjss1  3896  mpteq12dva  3994  axsep  4037  el  4086  euotd  4160  reusv1  4425  reusv2lem1  4426  reusv2lem2  4427  tfisi  4540  limom  4562  ssrelrel  4694  issref  4963  asymref2  4967  funmo  5129  funco  5149  funun  5153  fununi  5173  funcnvuni  5174  nfunsn  5410  funoprabg  5795  1stconst  6059  2ndconst  6060  frxp  6077  fnwelem  6082  iotaval  6154  iota5  6163  iotabidv  6164  seqomlem2  6349  iserd  6572  findcard3  6985  frfi  6987  fiint  7018  dffi2  7060  hartogslem1  7141  wdomd  7179  ixpiunwdom  7189  sucprcreg  7197  rankval3b  7382  fseqenlem2  7536  dfac3  7632  dfac5  7639  dfac2  7641  dfac8  7645  dfac9  7646  dfacacn  7651  dfac13  7652  kmlem1  7660  kmlem6  7665  kmlem13  7672  fin23lem32  7854  axdc2lem  7958  zornn0g  8016  brdom6disj  8041  fpwwe2lem11  8142  fpwwe2lem12  8143  fpwwe2lem13  8144  hargch  8179  alephgch  8180  nqpr  8518  reclem2pr  8552  shftfn  11445  fsumiunOLD  12158  hashiunOLD  12159  ramub  12934  ramcl  12950  imasaddfnlem  13304  imasvscafn  13313  catideu  13421  invfun  13510  mreclat  14125  letsr  14184  efgval  14861  efgi  14863  efgi2  14869  gsumval3  15026  gsumzaddlem  15038  pgpfac1lem5  15149  islbs3  15742  lbsextlem4  15746  mplsubglem  16011  mpllsslem  16012  cssmre  16425  obslbs  16462  tgcl  16539  indistopon  16570  ppttop  16576  epttop  16578  mretopd  16661  toponmre  16662  neissex  16696  lmfun  16941  2ndcdisj  17014  1stccnp  17020  kgentopon  17065  dfac14  17144  ptcnp  17148  uptx  17151  ptrescn  17165  qtoptop2  17222  filcon  17410  filssufilg  17438  rnelfmlem  17479  alexsubALTlem2  17574  prdsxmslem2  17907  mbfposr  18839  mbfinf  18852  i1fd  18868  itg1climres  18901  perfdvf  19085  evlseu  19232  taylf  19572  ex-natded9.26  20664  ex-natded9.26-2  20665  nmcexi  22436  relexpindlem  23207  rtrclreclem.min  23215  dfrtrcl2  23216  dfpo2  23282  dfon2lem6  23312  dfon2lem8  23314  dfon2lem9  23315  dfon2  23316  elfuns  23628  mptelee  23697  eqintg  24126  inposet  24444  inttop2  24681  intopcoaconb  24706  qusp  24708  prcnt  24717  ismonc  24980  isepic  24990  bosser  25333  trer  25393  finminlem  25397  neibastop1  25474  neibastop3  25477  upixp  25569  prter1  25913  ismrcd1  25939  ttac  26295  fnwe2  26316  aomclem6  26322  dfac11  26326  dfac21  26330  frlmup4  26419  hbtlem2  26494  sbeqalbi  26766  ax10ext  26772  ax10-16  26773  pm13.192  26777  pm14.24  26799  sbcss  26999  gen11  27078  trsspwALT2  27283  snssiALT  27293  sstrALT2  27301  en3lpVD  27311  sspwimp  27384  sspwimpcf  27386  sspwimpALT  27391  sspwimpALT2  27395  a9e2ndeqALT  27398  bnj145  27444  bnj1143  27511  bnj1379  27552  bnj149  27596
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