Theorem alrimiv 1927

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

Step	Hyp	Ref	Expression
1		ax-17 1579	. 2 |- ( ph -> A. x ph )
2		alrimiv.1	. 2 |- ( ph -> ps )
3	1, 2	alrimih 1522	1 |- ( ph -> A. x ps )

This proof depends on syntax axioms:   -> wi 4   A.wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1500  ax-gen 1502  ax-17 1579

This theorem is used by:  alrimivv  1928  nfdv  1930  sbbidv  1939  cbvalvw  1975  axext4  2222  eqrdv  2236  abbi2dv  2359  abbi1dv  2360  elex22  2837  elex2  2838  spcimdv  2909  spcimedv  2911  pm13.183  2964  sbcthdv  3066  sbcimdv  3117  ssrdv  3254  ss2abdv  3321  abssdv  3322  opprc  3925  dfnfc2  3953  intss  3991  intab  3999  dfiin2g  4045  disjss1  4112  sn0disj  4127  mpteq12dva  4213  el  4317  exmid1dc  4339  exmidn0m  4340  exmid0el  4343  exmidundif  4345  exmidundifim  4346  exmid1stab  4347  euotd  4397  reusv1  4606  elirr  4690  sucprcreg  4698  en2lp  4703  tfisi  4736  ssrelrel  4877  issref  5173  iotaval  5352  iota5  5362  iotabidv  5363  funmo  5395  funco  5420  funun  5425  fununfun  5427  fununi  5452  funcnvuni  5453  funimaexglem  5467  fvssunirng  5713  relfvssunirn  5714  sefvex  5719  nfunsn  5736  f1oresrab  5876  funoprabg  6190  uchoice  6375  mpofvex  6445  1stconst  6461  2ndconst  6462  disjxp1  6476  tfrexlem  6609  tfr1onlemsucfn  6615  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemaccex  6623  tfr1onlemres  6624  tfrcllemsucfn  6628  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemaccex  6636  tfrcllemres  6637  tfrcl  6639  rdgexggg  6652  rdgifnon  6654  rdgifnon2  6655  rdgivallem  6656  frecabcl  6674  frectfr  6675  frecrdg  6683  iserd  6837  fsetdmprc0  6954  modom  7112  exmidpw  7219  exmidpweq  7220  exmidpw2en  7223  fiintim  7242  fisseneq  7246  sbthlemi3  7281  finomni  7486  exmidomniim  7487  exmidomni  7488  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidmotap  7633  cc1  7637  pitonn  8221  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  zfz1iso  11315  shftfn  11611  ballotfilem2  13286  exmidunben  13375  imasex  13685  imasaddfnlemg  13694  prdsex  14279  lssex  14800  tgcl  15290  epttop  15316  neissex  15391  uptx  15500  dvfgg  15914  upgrspanop  16729  umgrspanop  16730  usgrspanop  16731  2spim  16999  decidr  17029  bj-om  17168  bj-nnord  17189  bj-inf2vn  17205  bj-inf2vn2  17206  bj-findis  17210  exmidsbthrlem  17273  sbthom  17277