Theorem cla4v 1865

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 groups:   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 1859	. 2 |- (A e. V -> (A.xph -> ps))
4	1, 3	ax-mp 7	1 |- (A.xph -> ps)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 953   = wceq 955   e. wcel 957  Vcvv 1808

This theorem is referenced by:  csbiegft 2026  rext 2750  frc 2916  relop 3271  pw2en 4435  pssnn 4522  unifi 4541  fiint 4543  fodomfi 4549  dfom3 4613  elom3 4614  aceq3lem 4715  aceq3 4716  aceq5lem4 4721  kmlem1 4748  kmlem4 4751  kmlem10 4757  zorn2lem7 4777  prlem934a 5120  suppsrlem 5204  nnunb 6027  dfuz 6160  chlim 9059

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809

Copyright terms: Public domain