Theorem spcv 2867

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 2860	. 2 |- ( A e. _V -> ( A. x ph -> ps ) )
4	1, 3	ax-mp 5	1 |- ( A. x ph -> ps )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1371   = wceq 1373   e. wcel 2176   _Vcvv 2772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774

This theorem is referenced by:  morex  2957  exmidexmid  4240  exmidsssn  4246  exmidel  4249  rext  4259  ontr2exmid  4573  regexmidlem1  4581  reg2exmid  4584  relop  4828  uchoice  6223  disjxp1  6322  rdgtfr  6460  ssfiexmid  6973  domfiexmid  6975  diffitest  6984  findcard  6985  exmidpw2en  7009  fiintim  7028  fisseneq  7031  finomni  7242  exmidomni  7244  exmidlpo  7245  exmidunben  12797  ivthreinc  15117  bj-d0clsepcl  15861  bj-inf2vnlem1  15906  subctctexmid  15937