Theorem alrimiv 1923

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 1575	. 2 |- ( ph -> A. x ph )
2		alrimiv.1	. 2 |- ( ph -> ps )
3	1, 2	alrimih 1518	1 |- ( ph -> A. x ps )

Syntax hints:   -> wi 4   A.wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1496  ax-gen 1498  ax-17 1575

This theorem is referenced by:  alrimivv  1924  nfdv  1926  sbbidv  1935  cbvalvw  1971  axext4  2218  eqrdv  2232  abbi2dv  2355  abbi1dv  2356  elex22  2831  elex2  2832  spcimdv  2903  spcimedv  2905  pm13.183  2957  sbcthdv  3059  sbcimdv  3110  ssrdv  3246  ss2abdv  3313  abssdv  3314  opprc  3906  dfnfc2  3934  intss  3972  intab  3980  dfiin2g  4026  disjss1  4093  mpteq12dva  4193  el  4293  exmid1dc  4315  exmidn0m  4316  exmid0el  4319  exmidundif  4321  exmidundifim  4322  exmid1stab  4323  euotd  4373  reusv1  4581  elirr  4665  sucprcreg  4673  en2lp  4678  tfisi  4711  ssrelrel  4852  issref  5147  iotaval  5326  iota5  5336  iotabidv  5337  funmo  5369  funco  5394  funun  5399  fununfun  5401  fununi  5426  funcnvuni  5427  funimaexglem  5441  fvssunirng  5687  relfvssunirn  5688  sefvex  5693  nfunsn  5709  f1oresrab  5844  funoprabg  6154  uchoice  6333  mpofvex  6403  1stconst  6419  2ndconst  6420  disjxp1  6434  tfrexlem  6567  tfr1onlemsucfn  6573  tfr1onlemsucaccv  6574  tfr1onlembxssdm  6576  tfr1onlembfn  6577  tfr1onlemaccex  6581  tfr1onlemres  6582  tfrcllemsucfn  6586  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  tfrcllembfn  6590  tfrcllemaccex  6594  tfrcllemres  6595  tfrcl  6597  rdgexggg  6610  rdgifnon  6612  rdgifnon2  6613  rdgivallem  6614  frecabcl  6632  frectfr  6633  frecrdg  6641  iserd  6795  modom  7063  exmidpw  7170  exmidpweq  7171  exmidpw2en  7174  fiintim  7193  fisseneq  7197  sbthlemi3  7231  finomni  7433  exmidomniim  7434  exmidomni  7435  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  exmidmotap  7577  cc1  7581  pitonn  8165  frecuzrdgtcl  10778  frecuzrdgfunlem  10785  zfz1iso  11217  shftfn  11513  ballotfilem2  13149  exmidunben  13194  prdsex  13499  imasex  13535  imasaddfnlemg  13544  lssex  14519  tgcl  14946  epttop  14972  neissex  15047  uptx  15156  dvfgg  15570  upgrspanop  16295  umgrspanop  16296  usgrspanop  16297  2spim  16555  decidr  16585  bj-om  16724  bj-nnord  16745  bj-inf2vn  16761  bj-inf2vn2  16762  bj-findis  16766  exmidsbthrlem  16819  sbthom  16823