Theorem ceqsalv 3141

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 1683	. 2 |- F/ x ps
2		ceqsalv.1	. 2 |- A e. _V
3		ceqsalv.2	. 2 |- ( x = A -> ( ph <-> ps ) )
4	1, 2, 3	ceqsal 3140	1 |- ( A. x ( x = A -> ph ) <-> ps )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1377   = wceq 1379   e. wcel 1767   _Vcvv 3113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3115

This theorem is referenced by:  ralxpxfr2d  3228  clel2  3240  clel4  3243  reu8  3299  frsn  5069  raliunxp  5140  fv3  5877  funimass4  5916  marypha2lem3  7893  kmlem12  8537  fpwwe2lem12  9015  vdwmc2  14352  itg2leub  21876  nmoubi  25363  choc0  25920  nmopub  26503  nmfnleub  26520  heibor1lem  29908