Theorem ceqsalv 2886

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 2885	1 |- (A.x(x = A -> ph) <-> ps)

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

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 2862

This theorem is referenced by:  clel2  2976  clel4  2979  reu8  3033  eqpw1  4163  pw111  4171  ssrelk  4212  eqrelk  4213  elp6  4264  sikexlem  4296  insklem  4305  nnadjoin  4521  nnadjoinpw  4522  nnpweq  4524  tfinnn  4535  raliunxp  4824  ssopr  4847  intirr  5030  fv3  5342  funimass4  5369  dfnnc3  5886  spacind  6288