Theorem ceqsalv 3121

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

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1379   = wceq 1381   e. wcel 1802   _Vcvv 3093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-12 1838  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-v 3095

This theorem is referenced by:  ralxpxfr2d  3208  clel2  3220  clel4  3223  reu8  3279  frsn  5057  raliunxp  5129  fv3  5866  funimass4  5906  marypha2lem3  7896  kmlem12  8541  fpwwe2lem12  9019  vdwmc2  14371  itg2leub  22011  nmoubi  25556  choc0  26113  nmopub  26696  nmfnleub  26713  heibor1lem  30277