Theorem spcgv 2776

Description: Rule of specialization, using implicit substitution. Compare Theorem 7.3 of [Quine] p. 44. (Contributed by NM, 22-Jun-1994.)

Hypothesis

Ref	Expression
spcgv.1	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
spcgv	|- ( A e. V -> ( A. x ph -> ps ) )

Distinct variable groups:   ps, x   x, A

Allowed substitution hints:   ph( x)   V( x)

Proof of Theorem spcgv

Step	Hyp	Ref	Expression
1		nfcv 2282	. 2 |- F/_ x A
2		nfv 1509	. 2 |- F/ x ps
3		spcgv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
4	1, 2, 3	spcgf 2771	1 |- ( A e. V -> ( A. x ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1330   = wceq 1332   e. wcel 1481

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691

This theorem is referenced by:  spcv  2783  mob2  2868  intss1  3794  dfiin2g  3854  exmidsssnc  4134  frirrg  4280  frind  4282  alxfr  4390  elirr  4464  en2lp  4477  tfisi  4509  mptfvex  5514  tfrcl  6269  rdgisucinc  6290  frecabex  6303  fisseneq  6828  mkvprop  7040  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  acfun  7080  ccfunen  7096  zfz1isolem1  10615  zfz1iso  10616  uniopn  12207  exmid1stab  13368  pw1nct  13371  sbthom  13396