Theorem cla4v 1400

Description: Rule of specialization with implicit substitution.

Hypotheses

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

Assertion

Ref	Expression
cla4v	|- (A.xph -> ps)

Distinct variable group(s):   x,A   ps,x

Proof of Theorem cla4v

Step	Hyp	Ref	Expression
1		cla4v.1	. 2 |- A e. V
2		cla4v.2	. . 3 |- (x = A -> (ph <-> ps))
3	2	cla4gv 1396	. 2 |- (A e. V -> (A.xph -> ps))
4	1, 3	ax-mp 6	1 |- (A.xph -> ps)

Syntax hints:   -> wi 2   <-> wb 127  A.wal 672   = wceq 1091   e. wcel 1092  Vcvv 1348

This theorem is referenced by:  cla4ev 1401  rext 1862  fri 2170  frc 2172  pw2en 3348  pssnn 3428  fiint 3445  dfom3 3477  elom3 3478  aceq3lem 3555  aceq3 3556  aceq5lem4 3561  kmlem1 3580  kmlem4 3583  kmlem9 3588  zornlem7 3609  prlem934a 3931  suppsrlem 4015  nnunb 4520  chlim 5139

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org