Theorem ceqsalv 2989

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

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1360   = wceq 1362   e. wcel 1755   _Vcvv 2962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-v 2964

This theorem is referenced by:  ralxpxfr2d  3073  clel2  3085  clel4  3088  reu8  3144  frsn  4896  raliunxp  4966  fv3  5691  funimass4  5730  marypha2lem3  7675  kmlem12  8318  fpwwe2lem12  8796  vdwmc2  14023  itg2leub  21054  nmoubi  23995  choc0  24552  nmopub  25135  nmfnleub  25152  heibor1lem  28552