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  2958  sbcthdv  3060  sbcimdv  3111  ssrdv  3248  ss2abdv  3315  abssdv  3316  opprc  3909  dfnfc2  3937  intss  3975  intab  3983  dfiin2g  4029  disjss1  4096  mpteq12dva  4196  el  4296  exmid1dc  4318  exmidn0m  4319  exmid0el  4322  exmidundif  4324  exmidundifim  4325  exmid1stab  4326  euotd  4376  reusv1  4584  elirr  4668  sucprcreg  4676  en2lp  4681  tfisi  4714  ssrelrel  4855  issref  5150  iotaval  5329  iota5  5339  iotabidv  5340  funmo  5372  funco  5397  funun  5402  fununfun  5404  fununi  5429  funcnvuni  5430  funimaexglem  5444  fvssunirng  5690  relfvssunirn  5691  sefvex  5696  nfunsn  5712  f1oresrab  5847  funoprabg  6160  uchoice  6344  mpofvex  6414  1stconst  6430  2ndconst  6431  disjxp1  6445  tfrexlem  6578  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemaccex  6605  tfrcllemres  6606  tfrcl  6608  rdgexggg  6621  rdgifnon  6623  rdgifnon2  6624  rdgivallem  6625  frecabcl  6643  frectfr  6644  frecrdg  6652  iserd  6806  modom  7074  exmidpw  7181  exmidpweq  7182  exmidpw2en  7185  fiintim  7204  fisseneq  7208  sbthlemi3  7242  finomni  7444  exmidomniim  7445  exmidomni  7446  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidmotap  7591  cc1  7595  pitonn  8179  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  zfz1iso  11238  shftfn  11534  ballotfilem2  13172  exmidunben  13261  imasex  13569  imasaddfnlemg  13578  prdsex  14114  lssex  14628  tgcl  15055  epttop  15081  neissex  15156  uptx  15265  dvfgg  15679  upgrspanop  16404  umgrspanop  16405  usgrspanop  16406  2spim  16664  decidr  16694  bj-om  16833  bj-nnord  16854  bj-inf2vn  16870  bj-inf2vn2  16871  bj-findis  16875  exmidsbthrlem  16928  sbthom  16932