Theorem ceqsalv 3233

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

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   = wceq 1483   e. wcel 1990   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  ralxpxfr2d  3327  clel2  3339  clel4  3342  frsn  5189  raliunxp  5261  fv3  6206  funimass4  6247  marypha2lem3  8343  kmlem12  8983  fpwwe2lem12  9463  vdwmc2  15683  itg2leub  23501  nmoubi  27627  choc0  28185  nmopub  28767  nmfnleub  28784  elintfv  31662  heibor1lem  33608  elmapintrab  37882