Theorem spcv 2815

Description: Rule of specialization, using implicit substitution. (Contributed by NM, 22-Jun-1994.)

Hypotheses

Ref	Expression
spcv.1	|- A e. _V
spcv.2	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
spcv	|- ( A. x ph -> ps )

Distinct variable groups:   x, A   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem spcv

Step	Hyp	Ref	Expression
1		spcv.1	. 2 |- A e. _V
2		spcv.2	. . 3 |- ( x = A -> ( ph <-> ps ) )
3	2	spcgv 2808	. 2 |- ( A e. _V -> ( A. x ph -> ps ) )
4	1, 3	ax-mp 5	1 |- ( A. x ph -> ps )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1340   = wceq 1342   e. wcel 2135   _Vcvv 2721

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723

This theorem is referenced by:  morex  2905  exmidexmid  4169  exmidsssn  4175  exmidel  4178  rext  4187  ontr2exmid  4496  regexmidlem1  4504  reg2exmid  4507  relop  4748  disjxp1  6195  rdgtfr  6333  ssfiexmid  6833  domfiexmid  6835  diffitest  6844  findcard  6845  fiintim  6885  fisseneq  6888  finomni  7095  exmidomni  7097  exmidlpo  7098  exmidunben  12296  bj-d0clsepcl  13642  bj-inf2vnlem1  13687  subctctexmid  13715