Theorem cla4gv 1865

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

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

This theorem is referenced by:  cla4v 1871  moi2 1927  moi 1928  uniiunlem 2135  elinti 2546  intss1 2552  alxfr 2902  fri 2924  limomss 3143  nnlim 3150  isofrlem 3907  f1oweALT 3912  pssnn 4544  unifiOLD 4570  fodomfi 4575  fodomfiOLD 4576  uniopnt 7599  metcn4i 7969  chlim 9099  fipfil2 10550  cnfilca 10562

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815

Copyright terms: Public domain