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  4241  exmidsssn  4247  exmidel  4250  rext  4260  ontr2exmid  4574  regexmidlem1  4582  reg2exmid  4585  relop  4829  uchoice  6225  disjxp1  6324  rdgtfr  6462  ssfiexmid  6975  domfiexmid  6977  diffitest  6986  findcard  6987  exmidpw2en  7011  fiintim  7030  fisseneq  7033  finomni  7244  exmidomni  7246  exmidlpo  7247  exmidunben  12830  ivthreinc  15150  bj-d0clsepcl  15898  bj-inf2vnlem1  15943  subctctexmid  15974