Theorem ceqsalv 2885

Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993.)

Hypotheses

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

Assertion

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

Distinct variable groups:   x,A   ps,x

Allowed substitution hint:   ph(x)

Proof of Theorem ceqsalv

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 |- F/xps
2		ceqsalv.1	. 2 |- A e. _V
3		ceqsalv.2	. 2 |- (x = A -> (ph <-> ps))
4	1, 2, 3	ceqsal 2884	1 |- (A.x(x = A -> ph) <-> ps)

Syntax hints:   -> wi 4   <-> wb 176  A.wal 1540   = wceq 1642   e. wcel 1710  _Vcvv 2859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2861

This theorem is referenced by:  clel2  2975  clel4  2978  reu8  3032  eqpw1  4162  pw111  4170  ssrelk  4211  eqrelk  4212  elp6  4263  sikexlem  4295  insklem  4304  nnadjoin  4520  nnadjoinpw  4521  nnpweq  4523  tfinnn  4534  raliunxp  4823  ssopr  4846  intirr  5029  fv3  5341  funimass4  5368  dfnnc3  5885  spacind  6287