Theorem ceqsalv 3075

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

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1397   = wceq 1399   e. wcel 1836   _Vcvv 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-12 1872  ax-ext 2370

This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-v 3049

This theorem is referenced by:  ralxpxfr2d  3162  clel2  3174  clel4  3177  reu8  3233  frsn  4997  raliunxp  5068  fv3  5800  funimass4  5838  marypha2lem3  7830  kmlem12  8472  fpwwe2lem12  8948  vdwmc2  14518  itg2leub  22245  nmoubi  25825  choc0  26382  nmopub  26964  nmfnleub  26981  heibor1lem  30507