Theorem cla4gv 1860

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 970	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 970	. 2 |- (ps -> A.xps)
3		cla4gv.1	. 2 |- (x = A -> (ph <-> ps))
4	1, 2, 3	cla4gf 1858	1 |- (A e. B -> (A.xph -> ps))

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

This theorem is referenced by:  cla4v 1866  moi2 1922  moi 1923  uniiunlem 2130  elinti 2539  intss1 2545  alxfr 2893  fri 2915  limomss 3134  nnlim 3141  isofrlem 3898  f1oweALT 3903  pssnn 4526  unifi 4545  fodomfi 4553  uniopnt 7577  metcn4i 7955  chlim 9092  fipfil2 10533  cnfilca 10545

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 1459

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

Copyright terms: Public domain