Theorem cla4gv 1862

Description: Rule of specialization with implicit substitution. Compare Theorem 7.3 of [Quine] p. 44.

Hypothesis

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

Assertion

Ref	Expression
cla4gv	|- (A e. B -> (A.xph -> ps))

Distinct variable groups:   ps,x   x,A

Proof of Theorem cla4gv

Step	Hyp	Ref	Expression
1		ax-17 971	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 971	. 2 |- (ps -> A.xps)
3		cla4gv.1	. 2 |- (x = A -> (ph <-> ps))
4	1, 2, 3	cla4gf 1860	1 |- (A e. B -> (A.xph -> ps))

Syntax hints:   -> wi 3   <-> wb 146  A.wal 954   = wceq 956   e. wcel 958

This theorem is referenced by:  cla4v 1868  moi2 1924  moi 1925  uniiunlem 2132  elinti 2542  intss1 2548  alxfr 2896  fri 2918  limomss 3137  nnlim 3144  isofrlem 3901  f1oweALT 3906  pssnn 4534  unifiOLD 4557  fodomfiOLD 4566  uniopnt 7598  metcn4i 7972  chlim 9104  fipfil2 10564  fipfil2OLD 10565  cnfilca 10583  cnfilcaOLD 10584

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain